Commit e86e16d5 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Fix typo.

parent 5d8aef49
...@@ -399,7 +399,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) := ...@@ -399,7 +399,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
|match goal with (* Force [A] in [ex_intro] to deal with coercions. *) |match goal with (* Force [A] in [ex_intro] to deal with coercions. *)
| |- _ : ?A, _ => refine (@ex_intro A _ x (conj _ _)); [|] | |- _ : ?A, _ => refine (@ex_intro A _ x (conj _ _)); [|]
(* If the existentially quantified predicate is non-dependent and [x] (* If the existentially quantified predicate is non-dependent and [x]
is a hole, [refine] will generate an additional goal it. *) is a hole, [refine] will generate an additional goal. *)
| |- _ : ?A, _ => refine (@ex_intro A _ x (conj _ _));[shelve| |] | |- _ : ?A, _ => refine (@ex_intro A _ x (conj _ _));[shelve| |]
end; [env_reflexivity|go xs]] end; [env_reflexivity|go xs]]
end in end in
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment