diff options
| -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. |