From 93d9f3e232dd92aef3f6a46a16fb52d8e1b8221e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 17 Aug 2020 23:03:50 +0200
Subject: Tactic inversion: adding support for registration of an equality in
 Type.

---
 tactics/inv.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 4b94dd0e72..3ee52c6a48 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.")
 | _ ->
-- 
cgit v1.2.3


From d14abd0ae1204d728a877d81d9553f77127ade4f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 17 Aug 2020 23:26:37 +0200
Subject: Tactic replace: adding support for registration of an equality in
 Type.

---
 tactics/equality.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'tactics')

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
-- 
cgit v1.2.3