Merge PR #12847: Tactics inversion and replace work with eq in type

Reviewed-by: ppedrot

4 files changed, 38 insertions, 5 deletions

diff --git a/doc/changelog/04-tactics/12847-master+inversion-works-with-eq-in-type.rst b/doc/changelog/04-tactics/12847-master+inversion-works-with-eq-in-type.rst
new file mode 100644
index 0000000000..b444a2f436
--- /dev/null
+++ b/doc/changelog/04-tactics/12847-master+inversion-works-with-eq-in-type.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  :tacn:`replace` and :tacn:`inversion` support registration of a
+  :g:`core.identity`-like equality in :g:`Type`, such as HoTT's :g:`path`
+  (`#12847 <https://github.com/coq/coq/pull/12847>`_,
+  partially fixes `#12846 <https://github.com/coq/coq/issues/12846>`_,
+  by Hugo Herbelin).
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.")
 | _ ->
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.