diff options
| author | Pierre-Marie Pédrot | 2020-09-23 00:03:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-23 00:03:04 +0200 |
| commit | 23b0dbb3a0a71edd9ce2137e88b715c3e36e576f (patch) | |
| tree | 03e8ae44736165cedee10163aa33b4e2dd7c313d /tactics | |
| parent | 193ea58286a15849cd7caa7d87572beb12204645 (diff) | |
| parent | ac3b1c0cd55bd0d73dabf8f0332952a73cafaf35 (diff) | |
Merge PR #12847: Tactics inversion and replace work with eq in type
Reviewed-by: ppedrot
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 8 | ||||
| -rw-r--r-- | tactics/inv.ml | 14 |
2 files changed, 17 insertions, 5 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 8478c1957a..60e2db4dce 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/tactics/inv.ml b/tactics/inv.ml index 41899132a6..498a4cfc26 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -116,7 +116,11 @@ let make_inv_predicate env evd indf realargs id status concl = (* Now, we can recurse down this list, for each ai,(mkRel k) whether to push <Ai>(mkRel k)=ai (when Ai is closed). In any case, we carry along the rest of pairs *) - let eqdata = Coqlib.build_coq_eq_data () in + let eqdata = + try Coqlib.build_coq_eq_data () + with UserError _ -> + try Coqlib.build_coq_identity_data () + with UserError _ -> user_err (str "No registered equality.") in let rec build_concl eqns args n = function | [] -> it_mkProd concl eqns, Array.rev_of_list args | ai :: restlist -> @@ -351,8 +355,12 @@ let remember_first_eq id x = if !x == Logic.MoveLast then x := Logic.MoveAfter i let dest_nf_eq env sigma t = match EConstr.kind sigma t with | App (r, [| t; x; y |]) -> let open Reductionops in - let eq = Coqlib.lib_ref "core.eq.type" in - if isRefX sigma eq r then + let is_global_exists gr c = + Coqlib.has_ref gr && isRefX sigma (Coqlib.lib_ref gr) c + in + let is_eq = is_global_exists "core.eq.type" r in + let is_identity = is_global_exists "core.identity.type" r in + if is_eq || is_identity then (t, whd_all env sigma x, whd_all env sigma y) else user_err Pp.(str "Not an equality.") | _ -> |