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.

---
 test-suite/success/eqtacticsnois.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test-suite/success/eqtacticsnois.v

(limited to 'test-suite')

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