Tactic replace: adding support for registration of an equality in Type.

1 files changed, 15 insertions, 0 deletions

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.