diff options
| author | Hugo Herbelin | 2015-05-15 11:37:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-05-15 11:39:49 +0200 |
| commit | 5d015ae0d90fd7fd3d440acee6ccd501d8b63ba0 (patch) | |
| tree | e73fb685fea3bd4aa5a9eecde1df69c518acccf0 /test-suite/bugs/opened | |
| parent | 76c3b40482978fffca50f6f59e8bcae455680aba (diff) | |
| parent | 3fb81febe8efc34860688cac88a2267cfe298cf7 (diff) | |
Merge v8.5 into trunk
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
Diffstat (limited to 'test-suite/bugs/opened')
| -rw-r--r-- | test-suite/bugs/opened/4214.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/4214.v b/test-suite/bugs/opened/4214.v new file mode 100644 index 0000000000..3daf452132 --- /dev/null +++ b/test-suite/bugs/opened/4214.v @@ -0,0 +1,5 @@ +(* Check that subst uses all equations around *) +Goal forall A (a b c : A), b = a -> b = c -> a = c. +intros. +subst. +Fail reflexivity. |