diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/eqtacticsnois.v | 15 |
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. |