Nouvelle mouture du traducteur v7->v8

Option -v8 à coqtop lance coqtopnew
Le terminateur reste "." en v8
Ajout construction primitive CLetTuple/RLetTuple
Introduction typage dans le traducteur pour traduire les Case/Cases/Match
Ajout mutables dans RCases or ROrderedCase pour permettre la traduction
Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts
+ Bugs ou améliorations diverses
Raffinement affichage projections de Record/Structure.


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

1 files changed, 9 insertions, 4 deletions

diff --git a/parsing/termast.ml b/parsing/termast.ml
index 9f09c14bec..9cc66a37fe 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -222,14 +222,15 @@ let rec ast_of_raw = function
       (* Pour compatibilité des theories, il faut LAMBDALIST partout *)
       ope("LAMBDALIST",[ast_of_raw t;a])
 
-  | RCases (_,typopt,tml,eqns) ->
+  | RCases (_,(typopt,_),tml,eqns) ->
       let pred = ast_of_rawopt typopt in
       let tag = "CASES" in
-      let asttomatch = ope("TOMATCH", List.map ast_of_raw tml) in
+      let asttomatch =
+	ope("TOMATCH", List.map (fun (tm,_) -> ast_of_raw tm) tml) in
       let asteqns = List.map ast_of_eqn eqns in 
       ope(tag,pred::asttomatch::asteqns)
 	
-  | ROrderedCase (_,LetStyle,typopt,tm,[|bv|]) ->
+  | ROrderedCase (_,LetStyle,typopt,tm,[|bv|],_) ->
       let nvar' = function Anonymous -> nvar wildcard | Name id -> nvar id in
       let rec f l = function
         | RLambda (_,na,RHole _,c) -> f (nvar' na :: l) c
@@ -239,7 +240,7 @@ let rec ast_of_raw = function
       let eqn = ope ("EQN", [c;ope ("PATTCONSTRUCT",(nvar wildcard)::l)]) in
       ope ("FORCELET",[(ast_of_rawopt typopt);(ast_of_raw tm);eqn])
 
-  | ROrderedCase (_,st,typopt,tm,bv) ->
+  | ROrderedCase (_,st,typopt,tm,bv,_) ->
       let tag = match st with
 	| IfStyle -> "FORCEIF"
 	| RegularStyle -> "CASE"
@@ -250,6 +251,10 @@ let rec ast_of_raw = function
       ope(tag,(ast_of_rawopt typopt)
 	    ::(ast_of_raw tm)
 	    ::(Array.to_list (Array.map ast_of_raw bv)))
+
+  | RLetTuple (loc,nal,(na,typopt),tm,b) ->
+      error "Let tuple not supported in v7"
+
   | RRec (_,fk,idv,tyv,bv) ->
       let alfi = Array.map ast_of_ident idv in
       (match fk with