Ajout d'une version nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6451 85f007b7-540e-0410-9357-904b9bb8a0f7

22 files changed, 235 insertions, 0 deletions

diff --git a/test-suite/output/Cases.out8 b/test-suite/output/Cases.out8
new file mode 100644
index 000000000..b63ffd926
--- /dev/null
+++ b/test-suite/output/Cases.out8
@@ -0,0 +1,13 @@
+t_rect = 
+fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
+fix F (t : t) : P t :=
+  match t as t0 return (P t0) with
+  | k x x0 => f x0 (F x0)
+  end
+     : forall P : t -> Type,
+       (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
+
+     = (1, 3)
+     : (nat * nat)%type
+     = (1, 2)
+     : (nat * nat)%type
diff --git a/test-suite/output/Cases.v8 b/test-suite/output/Cases.v8
new file mode 100644
index 000000000..f62206358
--- /dev/null
+++ b/test-suite/output/Cases.v8
@@ -0,0 +1,6 @@
+(* Cases with let-in in constructors types *)
+
+Inductive t : Set :=
+    k : let x := t in x -> x.
+
+Print t_rect.
\ No newline at end of file
diff --git a/test-suite/output/Coercions.out8 b/test-suite/output/Coercions.out8
new file mode 100644
index 000000000..4b8aa355a
--- /dev/null
+++ b/test-suite/output/Coercions.out8
@@ -0,0 +1,6 @@
+P x
+     : Prop
+R x x
+     : Prop
+fun (x : foo) (n : nat) => x n
+     : foo -> nat -> nat
diff --git a/test-suite/output/Coercions.v8 b/test-suite/output/Coercions.v8
new file mode 100644
index 000000000..f3a09f3c2
--- /dev/null
+++ b/test-suite/output/Coercions.v8
@@ -0,0 +1,15 @@
+(* Submitted by Randy Pollack *)
+
+Record pred (S : Set) : Type :=  {sp_pred :> S -> Prop}.
+Record rel (S : Set) : Type :=  {sr_rel :> S -> S -> Prop}.
+
+Section testSection.
+Variables (S : Set) (P : pred S) (R : rel S) (x : S).
+Check (P x).
+Check (R x x).
+End testSection.
+
+(* Check the removal of coercions with target Funclass *)
+
+Record foo : Type :=  {D :> nat -> nat}.
+Check (fun (x : foo) (n : nat) => x n).
\ No newline at end of file
diff --git a/test-suite/output/Fixpoint.out8 b/test-suite/output/Fixpoint.out8
new file mode 100644
index 000000000..4dca551a0
--- /dev/null
+++ b/test-suite/output/Fixpoint.out8
@@ -0,0 +1,6 @@
+fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : 
+list B := match l with
+          | nil => nil (A:=B)
+          | a :: l0 => f a :: F A B f l0
+          end
+     : forall A B : Set, (A -> B) -> list A -> list B
diff --git a/test-suite/output/Fixpoint.v8 b/test-suite/output/Fixpoint.v8
new file mode 100644
index 000000000..09d5405fc
--- /dev/null
+++ b/test-suite/output/Fixpoint.v8
@@ -0,0 +1,8 @@
+Require Import List.
+
+Check
+  (fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : 
+   list B := match l with
+             | nil => nil
+             | a :: l => f a :: F _ _ f l
+             end).
\ No newline at end of file
diff --git a/test-suite/output/Implicit.out8 b/test-suite/output/Implicit.out8
new file mode 100644
index 000000000..38c5b827f
--- /dev/null
+++ b/test-suite/output/Implicit.out8
@@ -0,0 +1,10 @@
+compose (C:=nat) S
+     : (nat -> nat) -> nat -> nat
+ex_intro (P:=fun _ : nat => True) (x:=0) I
+     : ex (fun _ : nat => True)
+d2 = fun x : nat => d1 (y:=x)
+     : forall x x0 : nat, x0 = x -> x0 = x
+
+
+Arguments x, x0 are implicit
+Argument scopes are [nat_scope nat_scope _]
diff --git a/test-suite/output/Implicit.v8 b/test-suite/output/Implicit.v8
new file mode 100644
index 000000000..e18ae5513
--- /dev/null
+++ b/test-suite/output/Implicit.v8
@@ -0,0 +1,19 @@
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(* Suggested by Pierre Casteran (bug #169) *)
+(* Argument 3 is needed to typecheck and should be printed *)
+Definition compose (A B C : Set) (f : A -> B) (g : B -> C) (x : A) := g (f x).
+Check (compose (C:=nat) S).
+
+(* Better to explicitly display the arguments inferable from a
+   position that could disappear after reduction *)
+Inductive ex (A : Set) (P : A -> Prop) : Prop :=
+    ex_intro : forall x : A, P x -> ex P.
+Check (ex_intro (P:=fun _ => True) (x:=0) I).
+
+(* Test for V8 printing of implicit by names *)
+Definition d1 y x (h : x = y :>nat) := h.
+Definition d2 x := d1 (y:=x).
+
+Print d2.
\ No newline at end of file
diff --git a/test-suite/output/InitSyntax.out8 b/test-suite/output/InitSyntax.out8
new file mode 100644
index 000000000..4ed72c506
--- /dev/null
+++ b/test-suite/output/InitSyntax.out8
@@ -0,0 +1,10 @@
+Inductive sig2 (A : Set) (P : A -> Prop) (Q : A -> Prop) : Set :=
+    exist2 : forall x : A, P x -> Q x -> sig2 P Q
+For sig2: Argument A is implicit
+For exist2: Argument A is implicit
+For sig2: Argument scopes are [type_scope type_scope type_scope]
+For exist2: Argument scopes are [type_scope _ _ _ _ _]
+exists x : nat, x = x
+     : Prop
+fun b : bool => if b then b else b
+     : bool -> bool
diff --git a/test-suite/output/InitSyntax.v8 b/test-suite/output/InitSyntax.v8
new file mode 100644
index 000000000..66a01e145
--- /dev/null
+++ b/test-suite/output/InitSyntax.v8
@@ -0,0 +1,4 @@
+(* Soumis par Pierre *)
+Print sig2.
+Check (exists x : nat, x = x).
+Check (fun b : bool => if b then b else b).
\ No newline at end of file
diff --git a/test-suite/output/Intuition.out8 b/test-suite/output/Intuition.out8
new file mode 100644
index 000000000..5831c9f43
--- /dev/null
+++ b/test-suite/output/Intuition.out8
@@ -0,0 +1,7 @@
+1 subgoal
+  
+  m : Z
+  n : Z
+  H : (m >= n)%Z
+  ============================
+   (m >= m)%Z
diff --git a/test-suite/output/Intuition.v8 b/test-suite/output/Intuition.v8
new file mode 100644
index 000000000..d9d35cabc
--- /dev/null
+++ b/test-suite/output/Intuition.v8
@@ -0,0 +1,5 @@
+Require Import ZArith_base.
+Goal forall m n : Z, (m >= n)%Z -> (m >= m)%Z /\ (m >= n)%Z.
+intros; intuition.
+Show.
+Abort.
\ No newline at end of file
diff --git a/test-suite/output/Nametab.out8 b/test-suite/output/Nametab.out8
new file mode 100644
index 000000000..f5e76e449
--- /dev/null
+++ b/test-suite/output/Nametab.out8
@@ -0,0 +1,28 @@
+Constant Top.Q.N.K.id (shorter name to refer to it is Q.N.K.id)
+Constant Top.Q.N.K.id (shorter name to refer to it is Q.N.K.id)
+Constant Top.Q.N.K.id (shorter name to refer to it is Q.N.K.id)
+Constant Top.Q.N.K.id
+Constant Top.Q.N.K.id (shorter name to refer to it is Q.N.K.id)
+No module is referred to by basename K
+No module is referred to by name N.K
+Module Top.Q.N.K
+Module Top.Q.N.K
+No module is referred to by basename N
+Module Top.Q.N
+Module Top.Q.N
+Module Top.Q
+Module Top.Q
+Constant Top.Q.N.K.id (shorter name to refer to it is K.id)
+Constant Top.Q.N.K.id
+Constant Top.Q.N.K.id (shorter name to refer to it is K.id)
+Constant Top.Q.N.K.id (shorter name to refer to it is K.id)
+Constant Top.Q.N.K.id (shorter name to refer to it is K.id)
+Module Top.Q.N.K
+No module is referred to by name N.K
+Module Top.Q.N.K
+Module Top.Q.N.K
+No module is referred to by basename N
+Module Top.Q.N
+Module Top.Q.N
+Module Top.Q
+Module Top.Q
diff --git a/test-suite/output/Nametab.v8 b/test-suite/output/Nametab.v8
new file mode 100644
index 000000000..e36881e86
--- /dev/null
+++ b/test-suite/output/Nametab.v8
@@ -0,0 +1,7 @@
+Module Q.
+  Module N.
+    Module K.
+      Definition id := Set.
+    End K.
+  End N.
+End Q.
\ No newline at end of file
diff --git a/test-suite/output/RealSyntax.out8 b/test-suite/output/RealSyntax.out8
new file mode 100644
index 000000000..e6f7556d9
--- /dev/null
+++ b/test-suite/output/RealSyntax.out8
@@ -0,0 +1,4 @@
+32%R
+     : R
+(-31)%R
+     : R
diff --git a/test-suite/output/RealSyntax.v8 b/test-suite/output/RealSyntax.v8
new file mode 100644
index 000000000..2e4feeef0
--- /dev/null
+++ b/test-suite/output/RealSyntax.v8
@@ -0,0 +1,3 @@
+Require Import Reals.
+Check 32%R.
+Check (-31)%R.
\ No newline at end of file
diff --git a/test-suite/output/Sum.out8 b/test-suite/output/Sum.out8
new file mode 100644
index 000000000..bda6a68b0
--- /dev/null
+++ b/test-suite/output/Sum.out8
@@ -0,0 +1,6 @@
+nat + nat + {True}
+     : Set
+{True} + {True} + {True}
+     : Set
+nat + {True} + {True}
+     : Set
diff --git a/test-suite/output/Sum.v8 b/test-suite/output/Sum.v8
new file mode 100644
index 000000000..c13f975b7
--- /dev/null
+++ b/test-suite/output/Sum.v8
@@ -0,0 +1,3 @@
+Check (nat + nat + {True}).
+Check ({True} + {True} + {True}).
+Check (nat + {True} + {True}).
\ No newline at end of file
diff --git a/test-suite/output/TranspModtype.out8 b/test-suite/output/TranspModtype.out8
new file mode 100644
index 000000000..41e8648bc
--- /dev/null
+++ b/test-suite/output/TranspModtype.out8
@@ -0,0 +1,10 @@
+TrM.A = M.A
+     : Set
+
+OpM.A = M.A
+     : Set
+
+TrM.B = M.B
+     : Set
+
+*** [ OpM.B : Set ]
diff --git a/test-suite/output/TranspModtype.v8 b/test-suite/output/TranspModtype.v8
new file mode 100644
index 000000000..27a1dff06
--- /dev/null
+++ b/test-suite/output/TranspModtype.v8
@@ -0,0 +1,22 @@
+Module Type SIG.
+  Axiom A : Set.
+  Axiom B : Set.
+End SIG.
+
+Module M : SIG.
+  Definition A := nat.
+  Definition B := nat.
+End M.
+
+Module N <: SIG := M.
+
+Module TranspId (X: SIG) <: SIG with Definition A := X.A := X.
+Module OpaqueId (X: SIG) : SIG with Definition A := X.A := X.
+
+Module TrM := TranspId M.
+Module OpM := OpaqueId M.
+
+Print TrM.A.
+Print OpM.A.
+Print TrM.B.
+Print OpM.B.
\ No newline at end of file
diff --git a/test-suite/output/ZSyntax.out8 b/test-suite/output/ZSyntax.out8
new file mode 100644
index 000000000..cbfb9f207
--- /dev/null
+++ b/test-suite/output/ZSyntax.out8
@@ -0,0 +1,26 @@
+32%Z
+     : Z
+fun f : nat -> Z => (f 0%nat + 0)%Z
+     : (nat -> Z) -> Z
+fun x : positive => Zpos (xO x)
+     : positive -> Z
+fun x : positive => (Zpos x + 1)%Z
+     : positive -> Z
+fun x : positive => Zpos x
+     : positive -> Z
+fun x : positive => Zneg (xO x)
+     : positive -> Z
+fun x : positive => (Zpos (xO x) + 0)%Z
+     : positive -> Z
+fun x : positive => (- Zpos (xO x))%Z
+     : positive -> Z
+fun x : positive => (- Zpos (xO x) + 0)%Z
+     : positive -> Z
+(Z_of_nat 0 + 1)%Z
+     : Z
+(0 + Z_of_nat (0 + 0))%Z
+     : Z
+Z_of_nat 0 = 0%Z
+     : Prop
+(0 + Z_of_nat 11)%Z
+     : Z
diff --git a/test-suite/output/ZSyntax.v8 b/test-suite/output/ZSyntax.v8
new file mode 100644
index 000000000..0412f6d68
--- /dev/null
+++ b/test-suite/output/ZSyntax.v8
@@ -0,0 +1,17 @@
+Require Import ZArith.
+Check 32%Z.
+Check (fun f : nat -> Z => (f 0%nat + 0)%Z).
+Check (fun x : positive => Zpos (xO x)).
+Check (fun x : positive => (Zpos x + 1)%Z).
+Check (fun x : positive => Zpos x).
+Check (fun x : positive => Zneg (xO x)).
+Check (fun x : positive => (Zpos (xO x) + 0)%Z).
+Check (fun x : positive => (- Zpos (xO x))%Z).
+Check (fun x : positive => (- Zpos (xO x) + 0)%Z).
+Check (Z_of_nat 0 + 1)%Z.
+Check (0 + Z_of_nat (0 + 0))%Z.
+Check (Z_of_nat 0 = 0%Z).
+
+(* Submitted by Pierre Casteran *)
+Require Import Arith.
+Check (0 + Z_of_nat 11)%Z.
\ No newline at end of file