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, 6 insertions, 4 deletions

diff --git a/interp/reserve.ml b/interp/reserve.ml
index f6f9fe60d3..5287ce5a2d 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -43,12 +43,14 @@ let rec unloc = function
   | RLambda (_,na,ty,c) -> RLambda (dummy_loc,na,unloc ty,unloc c)
   | RProd (_,na,ty,c) -> RProd (dummy_loc,na,unloc ty,unloc c)
   | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
-  | RCases (_,tyopt,tml,pl) ->
-      RCases (dummy_loc,option_app unloc tyopt,List.map unloc tml,
+  | RCases (_,(tyopt,rtntypopt),tml,pl) ->
+      RCases (dummy_loc,
+        (option_app unloc tyopt,ref (option_app unloc !rtntypopt)),
+	List.map (fun (tm,x) -> (unloc tm,x)) tml,
         List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
-  | ROrderedCase (_,b,tyopt,tm,bv) ->
+  | ROrderedCase (_,b,tyopt,tm,bv,x) ->
       ROrderedCase 
-      (dummy_loc,b,option_app unloc tyopt,unloc tm, Array.map unloc bv)
+      (dummy_loc,b,option_app unloc tyopt,unloc tm, Array.map unloc bv,x)
   | RRec (_,fk,idl,tyl,bv) ->
       RRec (dummy_loc,fk,idl,Array.map unloc tyl,Array.map unloc bv)
   | RCast (_,c,t) -> RCast (dummy_loc,unloc c,unloc t)