diff options
Diffstat (limited to 'test-suite/output/subst.v')
| -rw-r--r-- | test-suite/output/subst.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v index e48aa6bb28..91bdd03e02 100644 --- a/test-suite/output/subst.v +++ b/test-suite/output/subst.v @@ -45,4 +45,15 @@ Show. trivial. Qed. +(* A bug revealed by OCaml 4.03 warnings *) +Goal forall y, let x:=0 in y=x -> y=y. +intros * H; +subst. +Fail clear H. (* Was working *) +Abort. +Goal forall y, let x:=0 in y=x -> y=y. +intros * H; +subst. +Fail clear H. (* Was failing before fix *) +Abort. |