diff options
| author | Hugo Herbelin | 2017-04-06 10:10:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-30 11:24:53 +0200 |
| commit | edb21eab674b170d125a5b6fbc8213066b356d17 (patch) | |
| tree | 61816200330a54dc74fa3dee3ea71dcf98a561a6 /test-suite | |
| parent | 991b78fd9627ee76f1a1a39b8460bf361c6af53d (diff) | |
Fixing "decide equality"'s bug #5449.
The code was assuming that the terms t and u for which {t=u}+{t<>u} is
proved were distinct. We refine an internal "generalize" of "u" so
that it works on the two precise occurrences to abstract, even if
other occurrences of u occur as subterm of t too.
We also reuse the global constants found in the statement rather than
reconstructing them (this seems better in case the global constants
eventually get polymorphic universes?).
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/5449.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5449.v b/test-suite/bugs/closed/5449.v new file mode 100644 index 0000000000..d7fc2aaa00 --- /dev/null +++ b/test-suite/bugs/closed/5449.v @@ -0,0 +1,6 @@ +(* An example of decide equality which was failing due to a lhs dep into the rhs *) + +Require Import Coq.PArith.BinPos. +Goal forall x y, {Pos.compare_cont Gt x y = Gt} + {Pos.compare_cont Gt x y <> Gt}. +intros. +decide equality. |