diff options
| author | herbelin | 2009-12-03 23:09:05 +0000 |
|---|---|---|
| committer | herbelin | 2009-12-03 23:09:05 +0000 |
| commit | 7533b5b51bfaa580fb237591b0fc747e0172526d (patch) | |
| tree | 87f50625f2800903053eacc3d136a106402a2522 /test-suite | |
| parent | add340bfaa3fed3ae77956c510c291ed4f9b8646 (diff) | |
Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)
Removed one more bug in simplification of visibly_occur_id in r12549
+ improved CHANGES message
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12561 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Naming.out | 21 | ||||
| -rw-r--r-- | test-suite/output/Naming.v | 9 |
2 files changed, 23 insertions, 7 deletions
diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index 86055c3baf..105940a45d 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -1,11 +1,11 @@ 1 subgoal - + x3 : nat ============================ forall x x1 x4 x0 : nat, (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 1 subgoal - + x3 : nat x : nat x1 : nat @@ -15,14 +15,14 @@ ============================ x + x1 = x4 + x0 1 subgoal - + x3 : nat ============================ forall x x1 x4 x0 : nat, (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) -> x + x1 = x4 + x0 -> foo (S x) 1 subgoal - + x3 : nat ============================ forall x x1 x4 x0 : nat, @@ -32,7 +32,7 @@ x + x1 = x4 + x0 -> forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - + x3 : nat x : nat x1 : nat @@ -45,7 +45,7 @@ x + x1 = x4 + x0 -> forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - + x3 : nat x : nat x1 : nat @@ -58,7 +58,7 @@ ============================ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - + x3 : nat x : nat x1 : nat @@ -74,3 +74,10 @@ S : nat ============================ x5 + S = x6 + x7 + Datatypes.S x +1 subgoal + + x3 : nat + a : nat + H : a = 0 -> forall a : nat, a = 0 + ============================ + a = 0 diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v index 89e641ac99..327643dc57 100644 --- a/test-suite/output/Naming.v +++ b/test-suite/output/Naming.v @@ -80,3 +80,12 @@ before the intros and after (note the x5/x0 and the S0/S) *) Abort. + +(* Check naming in hypotheses *) + +Goal forall a, (a = 0 -> forall a, a = 0) -> a = 0. +intros. +Show. +apply H with (a:=a). (* test compliance with printing *) +Abort. + |