Réforme de l'interprétation des termes :

- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
  pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
  se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
  constrextern.ml est l'équivalent de termast.ml pour le nouveau
  printer; topconstr.ml; contient la définition de "constr_expr";
  modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid


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

2 files changed, 9 insertions, 9 deletions

diff --git a/syntax/PPCases.v b/syntax/PPCases.v
index 3bdf47feb0..356f6b2149 100644
--- a/syntax/PPCases.v
+++ b/syntax/PPCases.v
@@ -95,3 +95,4 @@ Syntax constr
                       [1 1] [<hov 0> $tomatch:L ] ]
               [1 0] "in " [<hov 0> $c:L ] ] ]
 .
+
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index ddfbceb835..d4d2ae5e63 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -83,7 +83,7 @@ Syntax constr
 (* Things parsed in command5 *)
 
   level 5:
-    cast [ ($C :: $T) ] -> [ [<hv 0> $C:L [0 0] "::" $T:E] ]
+    cast [ << (CAST $C $T) >> ] -> [ [<hv 0> $C:L [0 0] "::" $T:E] ]
   ;
 (* Things parsed in command6 *)
 
@@ -117,7 +117,7 @@ Syntax constr
   | lambdal_cons [ << (LAMLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body) >> ]
       -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) $id) $body)]
 
-  | pi [ ($x : $A)$B ] -> [ (PRODBOX (BINDERS) <<($x : $A)$B>>) ]
+  | pi [ << (PROD $A [$x]$B) >> ] -> [ (PRODBOX (BINDERS) (PROD $A [$x]$B)) ]
   | prodlist  [ << (PRODLIST $c $b) >> ]
        -> [(PRODBOX (BINDERS) (PRODLIST $c $b))]
 
@@ -125,7 +125,7 @@ Syntax constr
      -> [ [<hov 0> "(" [<hov 0> $pbi] ")" [0 1] $t:E ] ]
 
   | prod_cons
-      [ << (PRODBOX (BINDERS ($LIST $acc)) <:constr:<($x : $Dom)$body>>) >> ]
+      [ << (PRODBOX (BINDERS ($LIST $acc)) (PROD $Dom [$x]$body)) >> ]
       -> [(PRODBOX (BINDERS ($LIST $acc) (BINDER $Dom $x)) $body)]
   | prodl_start_cons [ << (PRODBOX $pbi (PRODLIST $Dom $Body)) >> ]
       -> [(PRODLBOX $pbi $Dom (IDS) $Body)]
@@ -138,17 +138,18 @@ Syntax constr
       -> [(PRODLBOX $pbi $c (IDS ($LIST $ids) $id) $body)]
 
 
-  | arrow [ $A -> $B ] -> [ [<hv 0> $A:L [0 0] "->" (ARROWBOX $B) ] ]
+  | arrow [ << (PROD $A [<>]$B) >> ] ->
+       [ [<hv 0> $A:L [0 0] "->" (ARROWBOX $B) ] ]
   | arrow_stop [ << (ARROWBOX $c) >> ] -> [ $c:E ]
-  | arrow_again [ << (ARROWBOX <:constr:< $A -> $B >>) >> ] ->
+  | arrow_again [ << (ARROWBOX (PROD $A [<>]$B)) >> ] ->
 	 [ $A:L [0 0] "->" (ARROWBOX $B) ]
 
 (* These are synonymous *)
 (* redundant
   | let [ [$x = $M]$N ] -> [ [<hov 0> "[" $x "=" $M:E "]" [0 1] $N:E ] ]
 *)
-  | letin [ [$x := $A]$B ] -> [ [ <hov 0> "[" $x ":=" $A:E "]" [0 1] $B:E ] ]
-  | letincast [ [$x := $A : $C]$B ] -> [ [ <hov 0> "[" $x ":=" $A:E ":" $C:E "]" [0 1] $B:E ] ]
+  | letin [ << (LETIN $A [$x]$B) >> ] -> [ [ <hov 0> "[" $x ":=" $A:E "]" [0 1] $B:E ] ]
+  | letincast [ << (LETIN (CAST $A $C) [$x]$B) >> ] -> [ [ <hov 0> "[" $x ":=" $A:E ":" $C:E "]" [0 1] $B:E ] ]
   ;
 
 (* Things parsed in command9 *)
@@ -261,5 +262,3 @@ Syntax constr
     evalconstr [ << (EVAL $c $r) >> ] ->
 	 [ [<hv 0> "Eval" [1 1] $r [1 0] "in" [1 1] $c:E ] ].
 
-
-