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, 367 insertions, 304 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index f8af13256..6d3974069 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -95,7 +95,7 @@ let pr_expl_args pr (a,expl) =
 
 let pr_opt_type pr = function
   | CHole _ -> mt ()
-  | t -> cut () ++ str ":" ++ pr (if !Options.p1 then ltop else (latom,E)) t
+  | t -> cut () ++ str ":" ++ pr t
 
 let pr_opt_type_spc pr = function
   | CHole _ -> mt ()
@@ -103,7 +103,7 @@ let pr_opt_type_spc pr = function
 
 let pr_name = function
   | Anonymous -> str"_"
-  | Name id -> pr_id id
+  | Name id -> pr_id (Constrextern.v7_to_v8_id id)
 
 let pr_located pr (loc,x) = pr x
 
@@ -139,67 +139,66 @@ let pr_binder pr (nal,t) =
     prlist_with_sep sep (pr_located pr_name) nal ++
     pr_opt_type pr t)
 *)
-(* Option 1a *)
-let pr_oneb pr t na =
-  match t with
-      CHole _ -> pr_located pr_name na
-    | _ -> hov 1
-        (str "(" ++  pr_located pr_name na ++ pr_opt_type pr t ++ str ")")
-let pr_binder1 pr (nal,t) =
-  hov 0 (prlist_with_sep sep (pr_oneb pr t) nal)
 
-let pr_binders1 pr bl =
-  hv 0 (prlist_with_sep sep (pr_binder1 pr) bl)
+let surround p = str"(" ++ p ++ str")"
 
-(* Option 1b *)
-let pr_binder1 pr (nal,t) =
+let pr_binder many pr (nal,t) =
   match t with
-      CHole _ -> prlist_with_sep sep (pr_located pr_name) nal
-    | _ -> hov 1
-	(str "(" ++ prlist_with_sep sep (pr_located pr_name) nal ++ str ":" ++
-	 pr ltop t ++ str ")")
-
-let pr_binders1 pr bl =
-  hv 0 (prlist_with_sep sep (pr_binder1 pr) bl)
-
-let pr_opt_type' pr = function
-  | CHole _ -> mt ()
-  | t -> cut () ++ str ":" ++ pr (latom,E) t
-
-let pr_prod_binders1 pr = function
-(*  | [nal,t] -> hov 1 (prlist_with_sep sep (pr_located pr_name) nal ++ pr_opt_type' pr t)*)
-  | bl -> pr_binders1 pr bl
+      CHole _ -> 
+        prlist_with_sep sep (pr_located pr_name) nal
+    | _ ->
+        let s = 
+          (prlist_with_sep sep (pr_located pr_name) nal ++ str ":" ++ pr t) in
+        hov 1 (if many then surround s else s)
+
+let pr_binder_among_many pr_c = function
+  | LocalRawAssum (nal,t) ->
+      pr_binder true pr_c (nal,t)
+  | LocalRawDef (na,c) ->
+      let c,topt = match c with
+        | CCast(_,c,t) -> c, t
+        | _ -> c, CHole dummy_loc in
+      hov 1 (surround
+        (pr_located pr_name na ++ pr_opt_type pr_c topt ++
+         str":=" ++ cut() ++ pr_c c))
+
+let pr_undelimited_binders pr_c =
+  prlist_with_sep sep (pr_binder_among_many pr_c)
+
+let pr_delimited_binders pr_c = function
+  | [LocalRawAssum (nal,t)] -> pr_binder false pr_c (nal,t)
+  | LocalRawAssum _ :: _ as bdl -> pr_undelimited_binders pr_c bdl
+  | _ -> assert false
 
-(* Option 2 *)
 let pr_let_binder pr x a =
   hov 0 (hov 0 (pr_name x ++ brk(0,1) ++ str ":=") ++ brk(0,1) ++ pr ltop a)
 
-let pr_binder2 pr (nal,t) =
-  hov 0 (
-    prlist_with_sep sep (pr_located pr_name) nal ++
-    pr_opt_type pr t)
-
-let pr_binders2 pr bl =
-  hv 0 (prlist_with_sep sep (pr_binder2 pr) bl)
-
-let pr_prod_binder2 pr (nal,t) =
-  str "forall " ++ hov 0 (
-    prlist_with_sep sep (pr_located pr_name) nal ++
-    pr_opt_type pr t) ++ str ","
-
-let pr_prod_binders2 pr bl =
-  hv 0 (prlist_with_sep sep (pr_prod_binder2 pr) bl)
-
-(**)
-let pr_binders pr = (if !Options.p1 then pr_binders1 else pr_binders2) pr
-let pr_prod_binders pr bl = 
-  if !Options.p1 then 
-    str "!" ++ pr_prod_binders1 pr bl ++ str "."
-  else
-    pr_prod_binders2 pr bl
-
+let rec extract_prod_binders = function
+  | CLetIn (loc,na,b,c) ->
+      let bl,c = extract_prod_binders c in
+      LocalRawDef (na,b) :: bl, c
+  | CProdN (loc,[],c) ->
+      extract_prod_binders c
+  | CProdN (loc,(nal,t)::bl,c) ->
+      let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
+      LocalRawAssum (nal,t) :: bl, c
+  | c -> [], c
+
+let rec extract_lam_binders = function
+  | CLetIn (loc,na,b,c) ->
+      let bl,c = extract_lam_binders c in
+      LocalRawDef (na,b) :: bl, c
+  | CLambdaN (loc,[],c) ->
+      extract_lam_binders c
+  | CLambdaN (loc,(nal,t)::bl,c) ->
+      let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
+      LocalRawAssum (nal,t) :: bl, c
+  | c -> [], c
+    
+(*
 let pr_arg_binders pr bl =
   if bl = [] then mt() else (spc() ++ pr_binders pr bl)
+*)
 
 let pr_global vars ref =
   (* pr_global_env vars ref *)
@@ -212,106 +211,20 @@ let split_lambda = function
   | CLambdaN (loc,(na::nal,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,t)::bl,c))
   | _ -> anomaly "ill-formed fixpoint body"
 
-let split_product = function
-  | CArrow (loc,t,c) -> ((loc,Anonymous),t,c)
-  | CProdN (loc,[[na],t],c) -> (na,t,c)
-  | CProdN (loc,([na],t)::bl,c) -> (na,t,CProdN(loc,bl,c))
-  | CProdN (loc,(na::nal,t)::bl,c) -> (na,t,CProdN(loc,(nal,t)::bl,c))
+let rename na na' t c =
+  match (na,na') with
+    | (_,Name id), (_,Name id') -> (na',t,replace_vars_constr_expr [id,id'] c)
+    | (_,Name id), (_,Anonymous) -> (na,t,c)
+    | _ -> (na',t,c)
+  
+let split_product na' = function
+  | CArrow (loc,t,c) -> (na',t,c)
+  | CProdN (loc,[[na],t],c) -> rename na na' t c
+  | CProdN (loc,([na],t)::bl,c) -> rename na na' t (CProdN(loc,bl,c))
+  | CProdN (loc,(na::nal,t)::bl,c) ->
+      rename na na' t (CProdN(loc,(nal,t)::bl,c))
   | _ -> anomaly "ill-formed fixpoint body"
 
-let rec extract_lam_binders c =
-  match c with
-      CLambdaN(loc,bl1,c') ->
-        let (bl,bd) = extract_lam_binders c' in
-        (bl1@bl, bd)
-    | _ -> ([],c)
-
-let rec extract_prod_binders c =
-  match c with
-      CProdN(loc,bl1,c') ->
-        let (bl,bd) = extract_prod_binders c' in
-        (bl1@bl, bd)
-    | _ -> ([],c)
-
-let rec check_same_pattern p1 p2 =
-  match p1, p2 with
-    | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) when i1=i2 ->
-        check_same_pattern a1 a2
-    | CPatCstr(_,c1,a1), CPatCstr(_,c2,a2) when c1=c2 ->
-        List.iter2 check_same_pattern a1 a2
-    | CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> ()
-    | CPatNumeral(_,i1), CPatNumeral(_,i2) when i1=i2 -> ()
-    | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 ->
-        check_same_pattern e1 e2
-    | _ -> failwith "not same pattern"
-
-let check_same_ref r1 r2 =
-  match r1,r2 with
-  | Qualid(_,q1), Qualid(_,q2) when q1=q2 -> ()
-  | Ident(_,i1), Ident(_,i2) when i1=i2 -> ()
-  | _ -> failwith "not same ref"
-
-let rec check_same_type ty1 ty2 =
-  match ty1, ty2 with
-  | CRef r1, CRef r2 -> check_same_ref r1 r2
-  | CFix(_,(_,id1),fl1), CFix(_,(_,id2),fl2) when id1=id2 ->
-      List.iter2 (fun (id1,i1,a1,b1) (id2,i2,a2,b2) ->
-        if id1<>id2 || i1<>i2 then failwith "not same fix";
-        check_same_type a1 a2;
-        check_same_type b1 b2)
-        fl1 fl2
-  | CCoFix(_,(_,id1),fl1), CCoFix(_,(_,id2),fl2) when id1=id2 ->
-      List.iter2 (fun (id1,a1,b1) (id2,a2,b2) ->
-        if id1<>id2 then failwith "not same fix";
-        check_same_type a1 a2;
-        check_same_type b1 b2)
-        fl1 fl2
-  | CArrow(_,a1,b1), CArrow(_,a2,b2) ->
-      check_same_type a1 a2;
-      check_same_type b1 b2
-  | CProdN(_,bl1,a1), CProdN(_,bl2,a2) ->
-      List.iter2 check_same_binder bl1 bl2;
-      check_same_type a1 a2
-  | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) ->
-      List.iter2 check_same_binder bl1 bl2;
-      check_same_type a1 a2
-  | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when na1=na2 ->
-      check_same_type a1 a2;
-      check_same_type b1 b2
-  | CAppExpl(_,r1,al1), CAppExpl(_,r2,al2) when r1=r2 ->
-      List.iter2 check_same_type al1 al2
-  | CApp(_,(_,e1),al1), CApp(_,(_,e2),al2) ->
-      check_same_type e1 e2;
-      List.iter2 (fun (a1,e1) (a2,e2) ->
-                    if e1<>e2 then failwith "not same expl";
-                    check_same_type a1 a2) al1 al2
-  | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) ->
-      List.iter2 check_same_type a1 a2;
-      List.iter2 (fun (_,pl1,r1) (_,pl2,r2) ->
-        List.iter2 check_same_pattern pl1 pl2;
-        check_same_type r1 r2) brl1 brl2
-  | COrderedCase(_,_,_,a1,bl1), COrderedCase(_,_,_,a2,bl2) ->
-      check_same_type a1 a2;
-      List.iter2 check_same_type bl1 bl2
-  | CHole _, CHole _ -> ()
-  | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> ()
-  | CSort(_,s1), CSort(_,s2) when s1=s2 -> ()
-  | CCast(_,a1,b1), CCast(_,a2,b2) ->
-      check_same_type a1 a2;
-      check_same_type b1 b2
-  | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 ->
-      List.iter2 check_same_type e1 e2
-  | CNumeral(_,i1), CNumeral(_,i2) when i1=i2 -> ()
-  | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 ->
-      check_same_type e1 e2
-  | _ when ty1=ty2 -> ()
-  | _ -> failwith "not same type"
-
-and check_same_binder (nal1,e1) (nal2,e2) =
-  List.iter2 (fun (_,na1) (_,na2) ->
-    if na1<>na2 then failwith "not same name") nal1 nal2;
-  check_same_type e1 e2
-
 let merge_binders (na1,ty1) (na2,ty2) =
   let na =
     match snd na1, snd na2 with
@@ -325,9 +238,9 @@ let merge_binders (na1,ty1) (na2,ty2) =
         CHole _, _ -> ty2
       | _, CHole _ -> ty1
       | _ ->
-          check_same_type ty1 ty2;
+          Constrextern.check_same_type ty1 ty2;
           ty2 in
-  ([na],ty)
+  LocalRawAssum ([na],ty)
             
 let rec strip_domain bvar c =
   match c with
@@ -358,13 +271,15 @@ let rec strip_domains (nal,ty) c =
 (* Re-share binders *)
 let rec factorize_binders = function
   | ([] | [_] as l) -> l
-  | (nal,ty)::((nal',ty')::l as l') ->
-      try
-	let _ = check_same_type ty ty' in
-	factorize_binders ((nal@nal',ty)::l)
+  | LocalRawAssum (nal,ty) as d :: (LocalRawAssum (nal',ty')::l as l') ->
+      (try
+	let _ = Constrextern.check_same_type ty ty' in
+	factorize_binders (LocalRawAssum (nal@nal',ty)::l)
       with _ ->
-	(nal,ty) :: factorize_binders l'
+	d :: factorize_binders l')
+  | d :: l -> d :: factorize_binders l
 
+(* Extrac lambdas when a type constraint occurs *)
 let rec extract_def_binders c ty =
   match c with
     | CLambdaN(loc,bvar::lams,b) ->
@@ -385,24 +300,29 @@ let rec split_fix n typ def =
   if n = 0 then ([],typ,def)
   else
     let (na,_,def) = split_lambda def in
-    let (_,t,typ) = split_product typ in
+    let (na,t,typ) = split_product na typ in
     let (bl,typ,def) = split_fix (n-1) typ def in
-    (([na],t)::bl,typ,def)
+    (LocalRawAssum ([na],t)::bl,typ,def)
 
 let pr_recursive_decl pr id b t c =
   pr_id id ++ b ++ pr_opt_type_spc pr t ++ str " :=" ++
   brk(1,2) ++ pr ltop c
 
+let name_of_binder = function
+  | LocalRawAssum (nal,_) -> nal
+  | LocalRawDef (_,_) -> []
+
 let pr_fixdecl pr (id,n,t0,c0) =
   let (bl,t,c) = extract_def_binders t0 c0 in
   let (bl,t,c) =
     if List.length bl <= n then split_fix (n+1) t0 c0 else (bl,t,c) in
   let annot =
-    let ids = List.flatten (List.map fst bl) in
+    let ids = List.flatten (List.map name_of_binder bl) in
     if List.length ids > 1 then 
       spc() ++ str "{struct " ++ pr_name (snd (list_last ids)) ++ str"}"
     else mt() in
-  pr_recursive_decl pr id (str" " ++ hov 0 (pr_binders pr bl) ++ annot) t c
+  pr_recursive_decl pr id
+    (str" " ++ hov 0 (pr_undelimited_binders (pr ltop) bl) ++ annot) t c
 
 let pr_cofixdecl pr (id,t,c) =
   pr_recursive_decl pr id (mt ()) t c
@@ -414,15 +334,35 @@ let pr_recursive pr_decl id = function
       prlist_with_sep (fun () -> fnl() ++ str "with ") pr_decl dl ++
       fnl() ++ str "for " ++ pr_id id
 
-let pr_annotation pr po =
-  match po with
-      None -> mt()
-    | Some p -> spc() ++ str "=> " ++ hov 0 (pr ltop p)
+let pr_arg pr x = spc () ++ pr x
 
-let pr_annotation2 pr po =
+let is_var id = function
+  | CRef (Ident (_,id')) when id=id' -> true
+  | _ -> false
+
+let pr_case_item pr (tm,(na,indnalopt)) =
+  hov 0 (pr (lcast,E) tm ++
+  (match na with
+    | Name id when not (is_var id tm) -> spc () ++ str "as " ++  pr_id id
+    | _ -> mt ()) ++
+  (match indnalopt with
+    | None -> mt ()
+    | Some (_,ind,nal) ->
+        spc () ++ str "in " ++ 
+        hov 0 (pr_reference ind ++ prlist (pr_arg pr_name) nal)))
+
+let pr_case_type pr po =
   match po with
-      None -> mt()
-    | Some p -> spc() ++ str "of type " ++ hov 0 (pr ltop p)
+    | None | Some (CHole _) -> mt()
+    | Some p -> spc() ++ str "return " ++ hov 0 (pr (lcast,E) p)
+
+let pr_return_type pr po = pr_case_type pr po
+
+let pr_simple_return_type pr na po =
+  (match na with
+    | Name id -> spc () ++ str "as " ++  pr_id id
+    | _ -> mt ()) ++
+  pr_case_type pr po
 
 let pr_proj pr pr_app a f l =
   hov 0 (pr lsimple a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
@@ -451,57 +391,68 @@ let rec pr inherited a =
       larrow
   | CProdN _ ->
       let (bl,a) = extract_prod_binders a in
-      hv 0 (pr_prod_binders pr bl ++ spc() ++ pr ltop a),
+      hov 2 (
+	str"forall" ++ spc() ++ pr_delimited_binders (pr ltop) bl ++
+        str "," ++ spc() ++ pr ltop a),
       lprod
   | CLambdaN _ ->
       let (bl,a) = extract_lam_binders a in
-      let left, mid = str"fun" ++ spc(), " =>" in
       hov 2 (
-	left ++ pr_binders pr bl ++
-        str mid ++ spc() ++ pr ltop a),
+	str"fun" ++ spc() ++ pr_delimited_binders (pr ltop) bl ++
+        str " =>" ++ spc() ++ pr ltop a),
       llambda
   | CLetIn (_,x,a,b) ->
-      let (bl,a) = extract_lam_binders a in
       hv 0 (
-        hov 2 (str "let " ++ pr_located pr_name x ++
-               pr_arg_binders pr bl ++ str " :=" ++ spc() ++
+        hov 2 (str "let " ++ pr_located pr_name x ++ str " :=" ++ spc() ++
                pr ltop a ++ str " in") ++
         spc () ++ pr ltop b),
       lletin
-  | CAppExpl (_,(true,f),l) ->
-      let a,l = list_sep_last l in
-      pr_proj pr pr_appexpl a f l, lapp
-  | CAppExpl (_,(false,f),l) -> pr_appexpl pr f l, lapp
-  | CApp (_,(true,a),l) ->
-      let c,l = list_sep_last l in
+  | CAppExpl (_,(Some i,f),l) ->
+      let l1,l2 = list_chop i l in
+      let c,l1 = list_sep_last l1 in
+      pr_proj pr pr_appexpl c f l1 ++
+      prlist (fun a -> spc () ++ pr (lapp,L) a) l2, lapp
+  | CAppExpl (_,(None,f),l) -> pr_appexpl pr f l, lapp
+  | CApp (_,(Some i,f),l) ->
+      let l1,l2 = list_chop i l in
+      let c,l1 = list_sep_last l1 in
       assert (snd c = None);
-      pr_proj pr pr_app (fst c) a l, lapp
-  | CApp (_,(false,a),l) -> pr_app pr a l, lapp
-  | CCases (_,po,c,eqns) ->
+      pr_proj pr pr_app (fst c) f l1 ++
+      prlist (fun a -> spc () ++ pr_expl_args pr a) l2, lapp
+  | CApp (_,(None,a),l) -> pr_app pr a l, lapp
+  | CCases (_,(po,rtntypopt),c,eqns) ->
       v 0
-        (hov 4 (str "match " ++ prlist_with_sep sep_v (pr ltop) c ++
-	(if !Options.p1 then pr_annotation pr po else mt ()) ++
-	str " with") ++
-        prlist (pr_eqn pr) eqns ++
-	(if !Options.p1 then mt () else pr_annotation2 pr po)
-	++ spc() ++ 
-	str "end"),
+        (hov 4 (str "match " ++ prlist_with_sep sep_v (pr_case_item pr) c
+        ++ pr_case_type pr rtntypopt ++ str " with") ++
+        prlist (pr_eqn pr) eqns ++ spc() ++ str "end"),
       latom
-  | COrderedCase (_,_,po,c,[b1;b2]) ->
+  | CLetTuple (_,nal,(na,po),c,b) ->
+      hv 0 (
+        str "let " ++
+	hov 0 (str "(" ++
+               prlist_with_sep sep_v pr_name nal ++
+               str ")" ++
+	       pr_simple_return_type pr na po ++ str " :=" ++
+               spc() ++ pr ltop c ++ str " in") ++
+        spc() ++ pr ltop b),
+      lletin
+      
+
+  | COrderedCase (_,st,po,c,[b1;b2]) when st = IfStyle ->
       (* On force les parenthèses autour d'un "if" sous-terme (même si le
 	 parsing est lui plus tolérant) *)
       hv 0 (
-	str "if " ++ pr ltop c ++ pr_annotation pr po ++ spc () ++
+	hov 1 (str "if " ++ pr ltop c ++ pr_return_type pr po) ++ spc () ++
 	hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++
 	hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2)),
       lif
-  | COrderedCase (_,_,po,c,[CLambdaN(_,[nal,_],b)]) ->
+  | COrderedCase (_,st,po,c,[CLambdaN(_,[nal,_],b)]) when st = LetStyle ->
       hv 0 (
         str "let " ++
 	hov 0 (str "(" ++
                prlist_with_sep sep_v (fun (_,n) -> pr_name n) nal ++
                str ")" ++
-	       pr_annotation pr po ++ str " :=" ++
+	       pr_return_type pr po ++ str " :=" ++
                spc() ++ pr ltop c ++ str " in") ++
         spc() ++ pr ltop b),
       lletin
@@ -509,7 +460,7 @@ let rec pr inherited a =
       hv 0 (
 	str (if style=MatchStyle then "old_match " else "match ") ++ 
 	pr ltop c ++
-	pr_annotation pr po ++
+	pr_return_type pr po ++
 	str " with" ++ brk (1,0) ++
 	hov 0 (prlist
           (fun b -> str "| ??? =>" ++ spc() ++ pr ltop b ++ fnl ()) bl) ++
@@ -530,21 +481,40 @@ let rec pr inherited a =
   if prec_less prec inherited then strm
   else str"(" ++ strm ++ str")"
 
-let transf env vars c =
+let rec strip_context n iscast t =
+  if n = 0 then
+    if iscast then match t with RCast (_,c,_) -> c | _ -> t else t
+  else match t with
+    | RLambda (_,_,_,c) -> strip_context (n-1) iscast c
+    | RProd (_,_,_,c) -> strip_context (n-1) iscast c
+    | RLetIn (_,_,_,c) -> strip_context (n-1) iscast c
+    | RCast (_,c,_) -> strip_context n false c
+    | _ -> anomaly "ppconstrnew: strip_context"
+
+let transf env n iscast c =
   if Options.do_translate() then
-    Constrextern.extern_rawconstr (Termops.vars_of_env env)
-      (Constrintern.for_grammar
+    let r = 
+      Constrintern.for_grammar
         (Constrintern.interp_rawconstr_gen false Evd.empty env [] false 
-	  (vars,[]))
-	c)
+	  ([],[]))
+	c in
+    begin try
+      (* Try to infer old case and type annotations *)
+      let _ = Pretyping.understand_gen_tcc Evd.empty env [] None r in 
+      (*msgerrnl (str "Typage OK");*) ()
+    with e -> (*msgerrnl (str "Warning: can't type")*) () end;
+    Constrextern.extern_rawconstr (Termops.vars_of_env env)
+      (strip_context n iscast r)
   else c
 
-let pr_constr_env env c = pr lsimple (transf env [] c)
-let pr_lconstr_env env c = pr ltop (transf env [] c)
+let pr_constr_env env c = pr lsimple (transf env 0 false c)
+let pr_lconstr_env env c = pr ltop (transf env 0 false c)
 let pr_constr c = pr_constr_env (Global.env()) c
 let pr_lconstr c = pr_lconstr_env (Global.env()) c
 
-let pr_lconstr_vars vars c = pr ltop (transf (Global.env()) vars c)
+let pr_lconstr_env_n env n b c = pr ltop (transf env n b c)
+
+let pr_binders = pr_undelimited_binders pr_lconstr
 
 let transf_pattern env c =
   if Options.do_translate() then
@@ -561,24 +531,10 @@ let pr_rawconstr_env env c =
 let pr_lrawconstr_env env c =
   pr_lconstr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c)
 
-let anonymize_binder na c =
-  if Options.do_translate() then
-    Constrextern.extern_rawconstr (Termops.vars_of_env (Global.env()))
-      (Reserve.anonymize_if_reserved na
-      (Constrintern.for_grammar
-        (Constrintern.interp_rawconstr Evd.empty (Global.env())) c))
-  else c
-
-let pr_binders l =
-  prlist_with_sep sep
-    (fun (nal,t) -> prlist_with_sep sep
-      (fun (_,na as x) -> pr_oneb pr (anonymize_binder na t) x) nal) l
-
 let pr_cases_pattern = pr_patt ltop
 
 let pr_occurrences prc (nl,c) =
-  prlist (fun n -> int n ++ spc ()) nl ++
-  str"(" ++ prc c ++ str")"
+   prc c ++ prlist (fun n -> spc () ++ int n) nl
 
 let pr_qualid qid = str (string_of_qualid qid)
 
@@ -604,7 +560,7 @@ let pr_metaid id = str"?" ++ pr_id id
 let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
   | Red false -> str "red"
   | Hnf -> str "hnf"
-  | Simpl o -> str "simpl" ++ pr_opt (pr_occurrences pr_lconstr) o  
+  | Simpl o -> str "simpl" ++ pr_opt (pr_occurrences pr_constr) o  
   | Cbv f ->
       if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then
 	str "compute"
@@ -613,12 +569,13 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
   | Lazy f -> 
       hov 1 (str "lazy" ++ pr_red_flag pr_ref f)
   | Unfold l ->
-      hov 1 (str "unfold" ++
-        prlist (fun (nl,qid) ->
-	  prlist (pr_arg int) nl ++ spc () ++ pr_ref qid) l)
+      hov 1 (str "unfold " ++
+        prlist_with_sep pr_coma (fun (nl,qid) ->
+	  pr_ref qid ++ prlist (pr_arg int) nl) l)
   | Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l)
   | Pattern l ->
-      hov 1 (str "pattern" ++ pr_arg (prlist (pr_occurrences pr_lconstr)) l)
+      hov 1 (str "pattern" ++
+        pr_arg (prlist_with_sep pr_coma (pr_occurrences pr_constr)) l)
         
   | Red true -> error "Shouldn't be accessible from user"
   | ExtraRedExpr (s,c) ->
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index cb2a1a677..40b122520 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -22,15 +22,16 @@ open Util
 open Genarg
 
 val extract_lam_binders :
-  constr_expr -> (name located list * constr_expr) list * constr_expr
+  constr_expr -> local_binder list * constr_expr
 val extract_prod_binders :
-  constr_expr -> (name located list * constr_expr) list * constr_expr
+  constr_expr -> local_binder list * constr_expr
 val extract_def_binders :
   constr_expr -> constr_expr ->
-  (name located list * constr_expr) list *  constr_expr * constr_expr
+  local_binder list * constr_expr * constr_expr
 val split_fix :
   int -> constr_expr -> constr_expr -> 
-  (name located list * constr_expr) list *  constr_expr * constr_expr
+  local_binder list *  constr_expr * constr_expr
+val pr_binders : local_binder list -> std_ppcmds
 
 val prec_less : int -> int * Ppextend.parenRelation -> bool
  
@@ -50,9 +51,8 @@ val pr_constr : constr_expr -> std_ppcmds
 val pr_lconstr : constr_expr -> std_ppcmds
 val pr_constr_env : env -> constr_expr -> std_ppcmds
 val pr_lconstr_env : env -> constr_expr -> std_ppcmds
-val pr_lconstr_vars : identifier list -> constr_expr -> std_ppcmds
+val pr_lconstr_env_n : env -> int -> bool -> constr_expr -> std_ppcmds
 val pr_cases_pattern : cases_pattern_expr -> std_ppcmds
-val pr_binders : (name located  list * constr_expr) list -> std_ppcmds
 val pr_may_eval :
   ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval
     -> std_ppcmds
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 6801aef28..80ac96492 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -23,6 +23,8 @@ open Genarg
 open Libnames
 open Pptactic
 
+let pr_id id = pr_id (Constrextern.v7_to_v8_id id)
+
 let pr_arg pr x = spc () ++ pr x
 
 let pr_ltac_constant sp = pr_qualid (Nametab.shortest_qualid_of_tactic sp)
@@ -48,7 +50,8 @@ let pr_binding prc = function
 let pr_esubst prc l =
   let pr_qhyp = function
       (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
-    | (_,NamedHyp id,c) -> str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")"
+    | (_,NamedHyp id,c) ->
+        str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")"
   in
   prlist_with_sep spc pr_qhyp l
 
@@ -171,8 +174,7 @@ let rec pr_tacarg_using_rule pr_gen = function
   | [], [] -> mt ()
   | _ -> failwith "Inconsistent arguments of extended tactic"
 
-let pr_then () =
-  if !Options.p1 then str " &" else str ";"
+let pr_then () = str ";"
 
 open Closure
 
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 95055c43c..f8ece8cea 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -37,8 +37,20 @@ let pr_reference r =
   try match Nametab.extended_locate (snd (qualid_of_reference r)) with
     | TrueGlobal ref ->
 	pr_reference (Constrextern.extern_reference dummy_loc Idset.empty ref)
-    | SyntacticDef sp ->
-	pr_reference r
+    | SyntacticDef kn ->
+	let is_coq_root d =
+	  let d = repr_dirpath d in
+	  d <> [] & string_of_id (list_last d) = "Coq" in
+        let dir,id = repr_path (sp_of_syntactic_definition kn) in
+	let r =
+          if (is_coq_root (Lib.library_dp()) or is_coq_root dir) then
+            (match string_of_id id with
+              | "refl_eqT" -> 
+		  Constrextern.extern_reference dummy_loc Idset.empty 
+		  (reference_of_constr (Coqlib.build_coq_eq_data ()).Coqlib.refl)
+              | _ -> r)
+          else r
+	in pr_reference r
   with Not_found ->
     error_global_not_found (snd (qualid_of_reference r))
 
@@ -96,6 +108,12 @@ let pr_entry_prec = function
   | Some Gramext.NonA -> str"NONA "
   | None -> mt()
 
+let pr_prec = function
+  | Some Gramext.LeftA -> str", left associativity"
+  | Some Gramext.RightA -> str", right associativity"
+  | Some Gramext.NonA -> str", no associativity"
+  | None -> mt()
+
 let pr_set_entry_type = function
   | ETIdent -> str"ident"
   | ETReference -> str"global"
@@ -132,8 +150,8 @@ let pr_search a b pr_c = match a with
 let pr_locality local = if local then str "Local " else str ""
 
 let pr_class_rawexpr = function
-  | FunClass -> str"FUNCLASS"
-  | SortClass -> str"SORTCLASS"
+  | FunClass -> str"Funclass"
+  | SortClass -> str"Sortclass"
   | RefClass qid -> pr_reference qid
 
 let pr_option_ref_value = function
@@ -224,7 +242,7 @@ let pr_with_declaration pr_c = function
 let rec pr_module_type pr_c = function
   | CMTEident qid -> pr_located pr_qualid qid
   | CMTEwith (mty,decl) ->
-      pr_module_type pr_c mty ++ spc() ++ str" with" ++
+      pr_module_type pr_c mty ++ spc() ++ str" with" ++ spc() ++
       pr_with_declaration pr_c decl
 
 let pr_of_module_type prc (mty,b) =
@@ -271,29 +289,17 @@ let anonymize_binder na c =
         (Constrintern.interp_rawconstr Evd.empty (Global.env())) c))
   else c
 
-let sep_fields () =
-  if !Options.p1 then fnl () else str ";" ++ spc ()
-
-let surround_binder p = 
-  if !Options.p1 then str"(" ++ p ++ str")" else p
+let surround p = str"(" ++ p ++ str")"
 
 let pr_binder pr_c ty na =
   match anonymize_binder (snd na) ty with
       CHole _ -> pr_located pr_name na
     | _ ->
         hov 1
-        (surround_binder (pr_located pr_name na ++ str":" ++ cut() ++ pr_c ty))
-
-let pr_valdecls pr_c = function
-  | LocalRawAssum (nal,c) ->
-      let sep = if !Options.p1 then spc else pr_tight_coma in
-      prlist_with_sep sep (pr_binder pr_c c) nal
-  | LocalRawDef (na,c) ->
-      hov 1
-        (surround_binder (pr_located pr_name na ++ str":=" ++ cut() ++ pr_c c))
+        (surround (pr_located pr_name na ++ str":" ++ cut() ++ pr_c ty))
 
-let pr_vbinders pr_c l =
-  hv 0 (prlist_with_sep spc (pr_valdecls pr_c) l)
+let pr_vbinders l =
+  hv 0 (pr_binders l)
 
 let vars_of_valdecls l = function
   | LocalRawAssum (nal,c) -> 
@@ -310,15 +316,27 @@ let vars_of_binder l (nal,_) =
 let vars_of_binders =
   List.fold_left vars_of_binder []
 
+let anonymize_binder na c =
+  if Options.do_translate() then
+    Constrextern.extern_rawconstr (Termops.vars_of_env (Global.env()))
+      (Reserve.anonymize_if_reserved na
+      (Constrintern.for_grammar
+        (Constrintern.interp_rawconstr Evd.empty (Global.env())) c))
+  else c
+
 let pr_sbinders sbl =
   if sbl = [] then mt () else
-    let bl = List.map (fun (id,c) -> ([(dummy_loc,Name id)],c)) sbl in
+    let bl =
+      List.map (fun (id,c) -> 
+        let c = anonymize_binder (Name id) c in
+        LocalRawAssum ([(dummy_loc,Name id)],c)) sbl in
     pr_binders bl ++ spc ()
 
 let pr_onescheme (id,dep,ind,s) =
-  pr_id id ++ str" :=" ++ spc() ++
-  (if dep then str"Induction for" else str"Minimality for")
-  ++ spc() ++ pr_reference ind ++ spc() ++ str"Sort" ++ spc() ++ pr_sort s
+  hov 0 (pr_id id ++ str" :=") ++ spc() ++
+  hov 0 ((if dep then str"Induction for" else str"Minimality for")
+  ++ spc() ++ pr_reference ind) ++ spc() ++ 
+  hov 0 (str"Sort" ++ spc() ++ pr_sort s)
 
 let pr_class_rawexpr = function
   | FunClass -> str"FUNCLASS"
@@ -340,14 +358,15 @@ let rec factorize = function
   | [] -> []
   | (c,(x,t))::l ->
       match factorize l with
-	| (xl,t')::l' when t' = (c,t) & not !Options.p1 -> (x::xl,t')::l'
+	| (xl,t')::l' when t' = (c,t) -> (x::xl,t')::l'
 	| l' -> ([x],(c,t))::l'
 
 let pr_ne_params_list pr_c l =
-  match factorize l with
-  | [params] -> surround_binder (pr_params pr_c params)
-  | l ->
-      prlist_with_sep spc (fun p -> str "(" ++ pr_params pr_c p ++ str ")") l
+  prlist_with_sep spc (fun p -> str "(" ++ pr_params pr_c p ++ str ")")
+(*
+  prlist_with_sep pr_semicolon (pr_params pr_c)
+*)
+    (factorize l)
 
 let pr_thm_token = function
   | Decl_kinds.Theorem -> str"Theorem"
@@ -416,7 +435,7 @@ let pr_syntax_entry (p,rl) =
   str"level" ++ spc() ++ int p ++ str" :" ++ fnl() ++
   prlist_with_sep (fun _ -> fnl() ++ str"| ") pr_syntax_rule rl
 
-let sep_end () = if !Options.p1 then str";" else str"."
+let sep_end () = str"."
 
 (**************************************)
 (* Pretty printer for vernac commands *)
@@ -449,7 +468,7 @@ let rec pr_vernac = function
   | VernacShow s -> 
       let pr_showable = function
 	| ShowGoal n -> str"Show" ++ pr_opt int n
-	| ShowGoalImplicitly n -> str"Show Implicits" ++ pr_opt int n
+	| ShowGoalImplicitly n -> str"Show Implicit Arguments" ++ pr_opt int n
 	| ShowProof -> str"Show Proof"
 	| ShowNode -> str"Show Node"
 	| ShowScript -> str"Show Script"
@@ -479,10 +498,16 @@ let rec pr_vernac = function
   | VernacVar id -> pr_id id
   
   (* Syntax *) 
-  | VernacGrammar _ -> str"(* <Warning> : Grammar is replaced by Notation *)"
+  | VernacGrammar _ -> 
+      msgerrnl (str"Warning : constr Grammar is discontinued; use Notation");
+      str"(* <Warning> : Grammar is replaced by Notation *)"
   | VernacTacticGrammar l -> hov 1 (str"Grammar tactic simple_tactic :=" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"|") pr_grammar_tactic_rule l) (***)
-  | VernacSyntax (u,el) -> hov 1 (str"Syntax " ++ str u ++ spc() ++
-    prlist_with_sep sep_v2 pr_syntax_entry el) (***)
+  | VernacSyntax (u,el) ->
+      msgerrnl (str"Warning : Syntax is discontinued; use Notation");
+      str"(* Syntax is discontinued " ++
+      hov 1 (str"Syntax " ++ str u ++ spc() ++
+      prlist_with_sep sep_v2 pr_syntax_entry el) ++ 
+      str " *)"
   | VernacOpenScope (local,sc) ->
       str "Open " ++ pr_locality local ++ str "Scope" ++ spc() ++ str sc
   | VernacDelimiters (sc,key) ->
@@ -496,8 +521,11 @@ let rec pr_vernac = function
       let (a,p,s) = match ov8 with
           Some mv8 -> mv8
         | None -> (a,p,s) in
-      hov 0 (str"Infix " ++ pr_locality local ++ pr_entry_prec a ++ int p
-        ++ spc() ++ qs s ++ spc() ++ pr_reference q ++ (match sn with
+      hov 0 (hov 0 (str"Infix " ++ pr_locality local
+      (* ++ pr_entry_prec a ++ int p ++ spc() *)
+      ++ qs s ++ spc() ++ pr_reference q) ++ spc()
+      ++ str "(at level " ++ int p ++ pr_prec a ++ str")" ++
+      (match sn with
     | None -> mt()
     | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
   | VernacDistfix (local,a,p,s,q,sn) ->
@@ -547,6 +575,20 @@ let rec pr_vernac = function
             str"Eval" ++ spc() ++
             pr_red_expr (pr_constr, pr_lconstr, pr_reference) r ++
             str" in" ++ spc() in
+      let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) in
+      let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) in
+      let rec abstract_rawconstr c = function
+        | [] -> c
+        | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_rawconstr c bl)
+        | LocalRawAssum (idl,t)::bl ->
+            List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
+            (abstract_rawconstr c bl) in
+      let rec prod_rawconstr c = function
+        | [] -> c
+        | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_rawconstr c bl)
+        | LocalRawAssum (idl,t)::bl ->
+            List.fold_right (fun x b -> mkProdC([x],t,b)) idl
+            (prod_rawconstr c bl) in
       let pr_def_body = function
         | DefineBody (bl,red,c,d) ->
             let (bl2,body,ty) = match d with
@@ -554,16 +596,25 @@ let rec pr_vernac = function
                   let bl2,body = extract_lam_binders c in
                   (bl2,body,mt())
               | Some ty ->
-                  let bl2,body,ty = extract_def_binders c ty in
-                  (bl2,body, spc() ++ str":" ++ pr_lconstrarg ty) in
+                  let bl2,body,ty' = extract_def_binders c ty in
+                  (bl2,body, spc() ++ str":" ++ spc () ++
+                    pr_lconstr_env_n (Global.env())
+                    (List.length (vars_of_vbinders bl @ vars_of_vbinders bl2))
+                    false (prod_rawconstr ty bl)) in
             let bindings =
-              pr_ne_sep spc (pr_vbinders pr_lconstr) bl ++
+              pr_ne_sep spc pr_vbinders bl ++
               if bl2 = [] then mt() else (spc() ++ pr_binders bl2) in
-	    let vars = vars_of_vbinders bl @ vars_of_binders bl2 in
-            let ppred = Some (pr_reduce red ++ pr_lconstr_vars vars body) in
+	    let vars = vars_of_vbinders bl @ vars_of_vbinders bl2 in
+	    let c',iscast = match d with None -> c, false
+	      | Some d -> CCast (dummy_loc,c,d), true in
+            let ppred =
+              Some (pr_reduce red ++
+              pr_lconstr_env_n (Global.env()) 
+                (List.length vars) iscast (abstract_rawconstr c' bl))
+            in
             (bindings,ty,ppred)
         | ProveBody (bl,t) ->
-            (pr_vbinders pr_lconstr bl, str" :" ++ pr_lconstrarg t, None) in
+            (pr_vbinders bl, str" :" ++ pr_lconstrarg t, None) in
       let (binds,typ,c) = pr_def_body b in
       hov 2 (pr_def_token e ++ spc() ++ pr_id id ++ binds ++ typ ++
       (match c with
@@ -574,7 +625,11 @@ let rec pr_vernac = function
       hov 1 (pr_thm_token ki ++ spc() ++ pr_id id ++ spc() ++
       (match bl with
         | [] -> mt()
-        | _ -> pr_vbinders pr_lconstr bl ++ spc()) ++ str":" ++ spc() ++ pr_lconstr c ++ sep_end () ++ str "Proof")
+        | _ -> error "Statements with local binders no longer supported")
+(*
+pr_vbinders bl ++ spc())
+*)
+      ++ str":" ++ spc() ++ pr_lconstr c) ++ sep_end () ++ fnl() ++ str "Proof"
   | VernacEndProof (opac,o) -> (match o with
     | None -> if opac then str"Qed" else str"Defined"
     | Some (id,th) -> (match th with
@@ -586,7 +641,8 @@ let rec pr_vernac = function
         (pr_assumption_token stre ++ spc() ++ pr_ne_params_list pr_lconstr l)
   | VernacInductive (f,l) ->
 
-      (* Copie simplifiée de command.ml pour recalculer les implicites *)
+      (* Copie simplifiée de command.ml pour recalculer les implicites, *)
+      (* les notations, et le contexte d'evaluation *)
       let lparams = match l with [] -> assert false | (_,_,la,_,_)::_ -> la in
       let nparams = List.length lparams
       and sigma = Evd.empty 
@@ -598,6 +654,32 @@ let rec pr_vernac = function
 	    (Termops.push_rel_assum (Name id,p) env,
 	    (Name id,None,p)::params))
 	  (env0,[]) lparams in
+
+      let (ind_env,ind_impls,arityl) =
+        List.fold_left
+          (fun (env, ind_impls, arl) (recname, _, _, arityc, _) ->
+            let arity = Constrintern.interp_type sigma env_params arityc in
+	    let fullarity =
+              Termops.prod_it arity (List.map (fun (id,_,ty) -> (id,ty)) params) in
+	    let env' = Termops.push_rel_assum (Name recname,fullarity) env in
+	    let impls = 
+	      if Impargs.is_implicit_args()
+	      then Impargs.compute_implicits false env_params fullarity
+	      else [] in
+	    (env', (recname,impls)::ind_impls, (arity::arl)))
+          (env0, [], []) l
+      in
+      let lparnames = List.map (fun (na,_,_) -> na) params in
+      let notations = 
+        List.map2 (fun (recname,ntnopt,_,_,_) ar ->
+          option_app (fun df ->
+            let larnames =
+	      List.rev_append lparnames 
+	        (List.rev (List.map fst (fst (Term.decompose_prod ar)))) in
+	    (recname,larnames,df)) ntnopt)
+          l arityl in
+      let ind_env_params = Environ.push_rel_context params ind_env in
+
       let lparnames = List.map (fun (na,_,_) -> na) params in
       let impl_ntns = List.map
 	(fun (recname,ntnopt,_,arityc,_) ->
@@ -629,8 +711,8 @@ let rec pr_vernac = function
 
       let pr_constructor (coe,(id,c)) =
         hov 2 (pr_id id ++ str" " ++
-               (if coe then str":>" else str":") ++
-               pr_lconstrarg c) in
+               (if coe then str":>" else str":") ++ spc () ++
+               pr_lconstr_env ind_env_params c) in
       let pr_constructor_list l = match l with
         | [] -> mt()
         | _ ->
@@ -657,6 +739,7 @@ let rec pr_vernac = function
   | VernacFixpoint recs ->
 
       (* Copie simplifiée de command.ml pour recalculer les implicites *)
+      (* les notations, et le contexte d'evaluation *)
       let sigma = Evd.empty
       and env0 = Global.env() in
       let impl_ntns = List.map
@@ -687,14 +770,24 @@ let rec pr_vernac = function
 	Metasyntax.add_notation_interpretation df
 	(AVar recname,larnames) scope) no) notations;
 
+      let rec_sign = 
+        List.fold_left 
+          (fun env ((recname,_,arityc,_),_) -> 
+            let arity = Constrintern.interp_type sigma env0 arityc in
+            Environ.push_named (recname,None,arity) env)
+          (Global.env()) recs in
+      
+      let name_of_binder = function
+        | LocalRawAssum (nal,_) -> nal
+        | LocalRawDef (_,_) -> [] in
       let pr_onerec = function
         | (id,n,type_0,def0),ntn ->
             let (bl,def,type_) = extract_def_binders def0 type_0 in
-            let ids = List.flatten (List.map fst bl) in
+            let ids = List.flatten (List.map name_of_binder bl) in
             let (bl,def,type_) =
               if List.length ids <= n then split_fix (n+1) def0 type_0
               else (bl,def,type_) in
-            let ids = List.flatten (List.map fst bl) in
+            let ids = List.flatten (List.map name_of_binder bl) in
             let annot =
               if List.length ids > 1 then 
                 spc() ++ str "{struct " ++
@@ -702,7 +795,9 @@ let rec pr_vernac = function
               else mt() in
             pr_id id ++ str" " ++ pr_binders bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr c) type_
-            ++ pr_decl_notation ntn ++ str" :=" ++ brk(1,1) ++ pr_lconstr def
+            ++ pr_decl_notation ntn ++ str" :=" ++ brk(1,1) ++
+            pr_lconstr_env_n rec_sign (List.length (vars_of_vbinders bl))
+	      true (CCast (dummy_loc,def0,type_0))
       in
       hov 1 (str"Fixpoint" ++ spc() ++
         prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)
@@ -717,32 +812,32 @@ let rec pr_vernac = function
       prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs)  
   | VernacScheme l ->
       hov 2 (str"Scheme" ++ spc() ++
-             prlist_with_sep (fun _ -> fnl() ++ str"with") pr_onescheme l)
+             prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l)
 
   (* Gallina extensions *)
-  | VernacRecord ((oc,name),ps,s,c,fs) ->
+  | VernacRecord (b,(oc,name),ps,s,c,fs) ->
       let pr_record_field = function
         | (oc,AssumExpr (id,t)) ->
-            hov 1 (surround_binder (pr_id id ++
+            hov 1 (pr_id id ++
             (if oc then str" :>" else str" :") ++ spc() ++
-            pr_lconstr t))
+            pr_lconstr t)
         | (oc,DefExpr(id,b,opt)) -> (match opt with
 	    | Some t ->
-                hov 1 (surround_binder (pr_id id ++
+                hov 1 (pr_id id ++
                 (if oc then str" :>" else str" :") ++ spc() ++
-                pr_lconstr t ++ str" :=" ++ pr_lconstr b))
+                pr_lconstr t ++ str" :=" ++ pr_lconstr b)
 	    | None ->
-                hov 1 (surround_binder (pr_id id ++ str" :=" ++ spc() ++
-                pr_lconstr b))) in
+                hov 1 (pr_id id ++ str" :=" ++ spc() ++
+                pr_lconstr b)) in
       hov 2
-        (str"Record" ++
+        (str (if b then "Record" else "Structure") ++
          (if oc then str" > " else str" ") ++ pr_id name ++ spc() ++
          pr_sbinders ps ++ str" :" ++ spc() ++ pr_lconstr s ++ str" := " ++
          (match c with
            | None -> mt()
-           | Some sc -> pr_id sc) ++ spc() ++ str"{" ++ cut() ++
-        hv 0 (prlist_with_sep sep_fields pr_record_field fs)
-        ++ str"}")
+           | Some sc -> pr_id sc) ++
+	spc() ++ str"{"  ++
+        hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}"))
   | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_id id)
   | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_id id)
   | VernacRequire (exp,spe,l) -> hov 2
@@ -789,7 +884,7 @@ let rec pr_vernac = function
   (* Solving *)
   | VernacSolve (i,tac,deftac) ->
       (if i = 1 then mt() else int i ++ str ": ") ++
-      (if !Options.p1 then mt () else str "By ") ++
+(*      str "By " ++*)
       (if deftac then mt() else str "!! ") ++
       Options.with_option Options.translate_syntax (pr_raw_tactic_goal i) tac
   | VernacSolveExistential (i,c) ->
@@ -833,9 +928,9 @@ let rec pr_vernac = function
 	  (Global.env())
 	  body in
       hov 1
-        ((if !Options.p1 then
+        (((*if !Options.p1 then
 	  (if rc then str "Recursive " else mt()) ++
-	  str "Tactic Definition " else
+	  str "Tactic Definition " else*)
 	    (* Rec by default *) str "Ltac ") ++
         prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
   | VernacHints (local,dbnames,h) -> pr_hints local dbnames h pr_constr
@@ -851,9 +946,9 @@ let rec pr_vernac = function
       hov 2 (str"Syntactic Definition " ++ pr_id id ++ str" :=" ++
              pr_lconstrarg c ++ spc() ++ str"|" ++ int n)
   | VernacDeclareImplicits (q,None) ->
-      hov 2 (str"Implicits" ++ spc() ++ pr_reference q)
+      hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
   | VernacDeclareImplicits (q,Some l) ->
-      hov 1 (str"Implicits" ++ spc() ++ pr_reference q ++ spc() ++
+      hov 1 (str"Implicit Arguments" ++ spc() ++ pr_reference q ++ spc() ++
              str"[" ++ prlist_with_sep sep int l ++ str"]")
   | VernacReserve (idl,c) ->
       hov 1 (str"Implicit Variable" ++
@@ -864,8 +959,17 @@ let rec pr_vernac = function
              spc() ++ prlist_with_sep sep pr_reference l)
   | VernacUnsetOption na ->
       hov 1 (str"Unset" ++ spc() ++ pr_printoption na None)
-  | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue true) -> str"Set Implicit Arguments"
-  | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue false) -> str"Unset Implicit Arguments"
+  | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue true) -> str"Set Implicit Arguments" 
+      ++
+      (if !Options.translate_strict_impargs then
+	sep_end () ++ fnl () ++ str"Unset Strict Implicits"
+      else mt ())
+  | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue false) -> 
+      str"Set Strict Implicits" 
+      ++
+      (if !Options.translate_strict_impargs then
+	sep_end () ++ fnl () ++ str"Unset Implicit Arguments"
+      else mt ())
   | VernacSetOption (na,v) -> hov 2 (str"Set" ++ spc() ++ pr_set_option na v)
   | VernacAddOption (na,l) -> hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l))
   | VernacRemoveOption (na,l) -> hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l))