diff options
| author | Pierre-Marie Pédrot | 2020-09-23 00:03:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-23 00:03:04 +0200 |
| commit | 23b0dbb3a0a71edd9ce2137e88b715c3e36e576f (patch) | |
| tree | 03e8ae44736165cedee10163aa33b4e2dd7c313d /test-suite | |
| parent | 193ea58286a15849cd7caa7d87572beb12204645 (diff) | |
| parent | ac3b1c0cd55bd0d73dabf8f0332952a73cafaf35 (diff) | |
Merge PR #12847: Tactics inversion and replace work with eq in type
Reviewed-by: ppedrot
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. |