diff options
| author | Maxime Dénès | 2018-12-21 15:11:52 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-09 11:18:31 +0100 |
| commit | 36500daa3efb746d3b19f288741c46b09b6d2632 (patch) | |
| tree | 9112268f8f8049aab9df131e6130c804ff0d801f | |
| parent | 62ece342f56380e54ecfe2b403159e9b115a8406 (diff) | |
Make some tests more robust by adding missing proof terminators
| -rw-r--r-- | test-suite/bugs/opened/bug_3166.v | 1 | ||||
| -rw-r--r-- | test-suite/bugs/opened/bug_3754.v | 1 | ||||
| -rw-r--r-- | test-suite/bugs/opened/bug_3938.v | 1 |
3 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/opened/bug_3166.v index e1c29a954c..baf87631f0 100644 --- a/test-suite/bugs/opened/bug_3166.v +++ b/test-suite/bugs/opened/bug_3166.v @@ -81,3 +81,4 @@ Goal forall T (x y : T) (p : x = y), True. compute in H0. change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0. Fail pose proof (fun k => @eq_trans _ _ _ k H0). +Abort. diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/opened/bug_3754.v index a717bbe735..18820b1a4c 100644 --- a/test-suite/bugs/opened/bug_3754.v +++ b/test-suite/bugs/opened/bug_3754.v @@ -282,3 +282,4 @@ Defined. rewrite <- ap_p_pp; rewrite_moveL_Mp_p. Set Debug Tactic Unification. Fail rewrite (concat_Ap ff2). + Abort. diff --git a/test-suite/bugs/opened/bug_3938.v b/test-suite/bugs/opened/bug_3938.v index 2d0d1930f1..3c7c945ed8 100644 --- a/test-suite/bugs/opened/bug_3938.v +++ b/test-suite/bugs/opened/bug_3938.v @@ -4,3 +4,4 @@ Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b. intros a b f H. rewrite H. (* Toplevel input, characters 15-25: Anomaly: Evar ?X11 was not declared. Please report. *) +Abort. |