diff options
author | 2016-12-22 19:45:04 +0100 | |
---|---|---|
committer | 2017-10-26 15:34:50 +0200 | |
commit | 91e9e1c26b7f2b874df83600b2bc8d23df9ed48b (patch) | |
tree | 770c08abffe9c2ea689cfa0f2e49cf9da445888c /test-suite/bugs/closed | |
parent | 925c434592597a34cd7ef4efb5e18a43e197bd96 (diff) |
Passing around the flag for injection so that tactics calling inj at
ML level can set the flags themselves.
In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".
This fixes bug #5281.
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r-- | test-suite/bugs/closed/5281.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5281.v b/test-suite/bugs/closed/5281.v new file mode 100644 index 000000000..03bafdc9a --- /dev/null +++ b/test-suite/bugs/closed/5281.v @@ -0,0 +1,6 @@ +Inductive A (T : Prop) := B (_ : T). +Scheme Equality for A. + +Goal forall (T:Prop), (forall x y : T, {x=y}+{x<>y}) -> forall x y : A T, {x=y}+{x<>y}. +decide equality. +Qed. |