diff options
Diffstat (limited to 'test-suite/output/subst.v')
| -rw-r--r-- | test-suite/output/subst.v | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v index 91bdd03e0..e48aa6bb2 100644 --- a/test-suite/output/subst.v +++ b/test-suite/output/subst.v @@ -45,15 +45,4 @@ 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. |