diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-29 09:35:07 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-29 15:29:17 +0200 |
| commit | 4e3d4646788c96f16193df14a81aa79938812194 (patch) | |
| tree | 01494f51829ec148926b7c7d8a8d19dab3cfce51 /test-suite | |
| parent | 4e93587fd83bab4ad5c158aa6b3c194e8a7a5551 (diff) | |
Fix a bug in subst releaved by an OCaml warning.
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, 219 insertions, 0 deletions
diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out index 209b2bc26..dbb9e09a4 100644 --- a/test-suite/output/subst.out +++ b/test-suite/output/subst.out @@ -26,6 +26,19 @@ 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 @@ -39,6 +52,45 @@ 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 @@ -52,6 +104,58 @@ 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 @@ -75,6 +179,19 @@ 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 @@ -88,6 +205,45 @@ 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 @@ -95,3 +251,55 @@ 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 e48aa6bb2..91bdd03e0 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. |