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 /tactics | |
| parent | 93d9f3e232dd92aef3f6a46a16fb52d8e1b8221e (diff) | |
Tactic replace: adding support for registration of an equality in Type.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 8 |
1 files changed, 6 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 |