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

4 files changed, 11 insertions, 8 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index 66ac7b97e9..7394a41c5d 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -180,7 +180,7 @@ let rawconstr_of_prog p =
 	let (bl',avoid',nenv') = push_vars avoid nenv bl in
 	let c1 = trad avoid nenv e1
 	and c2 = trad avoid' nenv' e2 in
-	ROrderedCase (dummy_loc, LetStyle, None, c1, [| raw_lambda bl' c2 |])
+	ROrderedCase (dummy_loc, LetStyle, None, c1, [| raw_lambda bl' c2 |], ref None)
 
     | CC_lam (bl,e) ->
 	let bl',avoid',nenv' = push_vars avoid nenv bl in
@@ -214,7 +214,7 @@ let rawconstr_of_prog p =
 	let c = trad avoid nenv b in
 	let cl = List.map (trad avoid nenv) el in
 	let ty = Detyping.detype (Global.env()) avoid nenv ty in
-	ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl)
+	ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl, ref None)
 
     | CC_expr c -> 
 	Detyping.detype (Global.env()) avoid nenv c
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 0e6b3b7d2f..2e3fcac411 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -107,7 +107,7 @@ open Coqast
 let mk_id loc id = mkRefC (Ident (loc, id))
 let mk_ref loc s = mk_id loc (id_of_string s)
 let mk_appl loc1 loc2 f args =
-  CApp (join_loc loc1 loc2, (false,mk_ref loc1 f), List.map (fun a -> a,None) args)
+  CApp (join_loc loc1 loc2, (None,mk_ref loc1 f), List.map (fun a -> a,None) args)
 
 let conj_assert {a_name=n;a_value=a} {a_value=b} = 
   let loc1 = constr_loc a in
@@ -166,7 +166,7 @@ let rec coqast_of_program loc = function
 		   (function Term t -> (coqast_of_program t.loc t.desc,None)
 		      | _ -> invalid_arg "coqast_of_program") l
       in
-      CApp (dummy_loc, (false,f), args)
+      CApp (dummy_loc, (None,f), args)
   | Expression c -> bdize c
   | _ -> invalid_arg "coqast_of_program"
 
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 487f45057c..3d01dd92fe 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -144,7 +144,7 @@ let (imply_intro1: pbp_rule) = function
 
 let make_var id = CRef (Ident(zz, id))
 
-let make_app f l = CApp (zz,(false,f),List.map (fun x -> (x,None)) l)
+let make_app f l = CApp (zz,(None,f),List.map (fun x -> (x,None)) l)
 
 let make_pbp_pattern x =
   make_app (make_var (id_of_string "PBP_META"))
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index c0ba10bddf..8d82da7e1f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -313,14 +313,17 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 	       xlate_formula_ne_list l)
    | CApp(_, (_,f), l) -> (* TODO: proj notation *)
        CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
-   | CCases (_,po,tml,eqns)-> CT_cases(xlate_formula_opt po, 
-                         xlate_formula_ne_list tml,
+   | CCases (_,(po,None),tml,eqns)-> CT_cases(xlate_formula_opt po, 
+                         xlate_formula_ne_list (List.map fst tml),
                          CT_eqn_list (List.map 
          (fun x -> translate_one_equation x)
 			   eqns))
+   | CCases (_,(po,Some _),tml,eqns)-> xlate_error "TODO"
    | COrderedCase (_,Term.IfStyle,po,c,[b1;b2]) -> 
 		   CT_if(xlate_formula_opt po,
                    xlate_formula c,xlate_formula b1,xlate_formula b2)		
+   | CLetTuple (_,l, (na,po), c, b) -> xlate_error "LetTuple: TODO"
+
    | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) ->
        CT_inductive_let(xlate_formula_opt po,
 	       xlate_id_opt_ne_list l,
@@ -1500,7 +1503,7 @@ let xlate_vernac =
 
   | (*Record from tactics/Record.v *)
     VernacRecord 
-      ((add_coercion, s), binders, CSort (_,c1), rec_constructor_or_none, field_list) ->
+      (_, (add_coercion, s), binders, CSort (_,c1), rec_constructor_or_none, field_list) ->
       let record_constructor = xlate_ident_opt rec_constructor_or_none in
       CT_record
        ((if add_coercion then CT_coercion_atm else