diff options
| author | Hugo Herbelin | 2020-08-17 23:26:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-18 09:16:17 +0200 |
| commit | d14abd0ae1204d728a877d81d9553f77127ade4f (patch) | |
| tree | 960784f73bd473c7443d027a5f43ca790e13ad7d | |
| parent | 93d9f3e232dd92aef3f6a46a16fb52d8e1b8221e (diff) | |
Tactic replace: adding support for registration of an equality in Type.
| -rw-r--r-- | tactics/equality.ml | 8 | ||||
| -rw-r--r-- | test-suite/success/eqtacticsnois.v | 15 |
2 files changed, 21 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 1689b0d3ad..282b72eb28 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -659,8 +659,12 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = | None -> tclFAIL 0 (str"Terms do not have convertible types") | Some evd -> - let e = lib_ref "core.eq.type" in - let sym = lib_ref "core.eq.sym" in + let e,sym = + try lib_ref "core.eq.type", lib_ref "core.eq.sym" + with UserError _ -> + try lib_ref "core.identity.type", lib_ref "core.identity.sym" + with UserError _ -> + user_err (strbrk "Need a registration for either core.eq.type and core.eq.sym or core.identity.type and core.identity.sym.") in Tacticals.New.pf_constr_of_global sym >>= fun sym -> Tacticals.New.pf_constr_of_global e >>= fun e -> let eq = applist (e, [t1;c1;c2]) in diff --git a/test-suite/success/eqtacticsnois.v b/test-suite/success/eqtacticsnois.v new file mode 100644 index 0000000000..7869532c67 --- /dev/null +++ b/test-suite/success/eqtacticsnois.v @@ -0,0 +1,15 @@ +(* coq-prog-args: ("-nois") *) + +Inductive eq {A : Type} (x : A) : forall a:A, Prop := eq_refl : eq x x. + +Axiom sym : forall A (x y : A) (_ : eq x y), eq y x. +Require Import Ltac. + +Register eq as core.eq.type. +Register sym as core.eq.sym. + +Goal forall A (x y:A) (_ : forall z, eq y z), eq x x. +intros * H. replace x with y. +- reflexivity. +- apply H. +Qed. |