diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 12:21:35 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 12:21:35 +0200 |
| commit | bff880ffb6ef33c99a96e7925c995b31b1497e6a (patch) | |
| tree | 1648e77d2abfdbfc3bbc567472e3835042e2dd69 /test-suite | |
| parent | 367e1f913f8d0b921dc4902b83d889dac3576580 (diff) | |
| parent | c78af970e1f003587fba9bebdf3ab5ca3b23face (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/subst.out | 208 | ||||
| -rw-r--r-- | test-suite/output/subst.v | 11 |
2 files changed, 0 insertions, 219 deletions
diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out index dbb9e09a4..209b2bc26 100644 --- a/test-suite/output/subst.out +++ b/test-suite/output/subst.out @@ -26,19 +26,6 @@ True 1 subgoal - y, z : nat - Hy : y = 0 - Hz : z = 0 - H1 : 0 = 1 - HA : True - H2 : 0 = 2 - H3 : y = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - x, y : nat Hx : x = 0 Hy : y = 0 @@ -52,45 +39,6 @@ True 1 subgoal - y, z : nat - Hy : y = 0 - Hz : z = 0 - H1 : 0 = 1 - HA : True - H2 : 0 = 2 - H3 : y = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - - x, z : nat - Hx : x = 0 - Hz : z = 0 - H1 : x = 1 - HA : True - H2 : x = 2 - H3 : 0 = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 - H1 : 0 = 1 - HA : True - H2 : 0 = 2 - H3 : y = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - H1 : 0 = 1 HA : True H2 : 0 = 2 @@ -104,58 +52,6 @@ y, z : nat Hy : y = 0 Hz : z = 0 - H1 : 0 = 1 - HA : True - H2 : 0 = 2 - H3 : y = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 - H1 : 0 = 1 - HA : True - H2 : 0 = 2 - H3 : y = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - - x, z : nat - Hx : x = 0 - Hz : z = 0 - H1 : x = 1 - HA : True - H2 : x = 2 - H3 : 0 = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 - H1 : 0 = 1 - HA : True - H2 : 0 = 2 - H3 : y = 3 - HB : True - H4 : z = 4 - ============================ - True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 HA : True H3 : y = 3 HB : True @@ -179,19 +75,6 @@ True 1 subgoal - y, z : nat - Hy : y = 0 - Hz : z = 0 - HA : True - H3 : y = 3 - HB : True - H4 : z = 4 - H1 : 0 = 1 - H2 : 0 = 2 - ============================ - True -1 subgoal - x, y : nat Hx : x = 0 Hy : y = 0 @@ -205,45 +88,6 @@ True 1 subgoal - y, z : nat - Hy : y = 0 - Hz : z = 0 - HA : True - H3 : y = 3 - HB : True - H4 : z = 4 - H1 : 0 = 1 - H2 : 0 = 2 - ============================ - True -1 subgoal - - x, z : nat - Hx : x = 0 - Hz : z = 0 - H1 : x = 1 - HA : True - H2 : x = 2 - HB : True - H4 : z = 4 - H3 : 0 = 3 - ============================ - True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 - HA : True - H3 : y = 3 - HB : True - H4 : z = 4 - H1 : 0 = 1 - H2 : 0 = 2 - ============================ - True -1 subgoal - HA, HB : True H4 : 0 = 4 H3 : 0 = 3 @@ -251,55 +95,3 @@ H2 : 0 = 2 ============================ True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 - HA : True - H3 : y = 3 - HB : True - H4 : z = 4 - H1 : 0 = 1 - H2 : 0 = 2 - ============================ - True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 - HA : True - H3 : y = 3 - HB : True - H4 : z = 4 - H1 : 0 = 1 - H2 : 0 = 2 - ============================ - True -1 subgoal - - x, z : nat - Hx : x = 0 - Hz : z = 0 - H1 : x = 1 - HA : True - H2 : x = 2 - HB : True - H4 : z = 4 - H3 : 0 = 3 - ============================ - True -1 subgoal - - y, z : nat - Hy : y = 0 - Hz : z = 0 - HA : True - H3 : y = 3 - HB : True - H4 : z = 4 - H1 : 0 = 1 - H2 : 0 = 2 - ============================ - True 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. |