modif des fixpoints pour que si on donne une notation au produit, les pts fixes s'affichent correctement

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

28 files changed, 541 insertions, 294 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 41ce1c4c1c..61d0d5a3af 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -34,7 +34,7 @@ and ct_COERCION_OPT =
 and ct_COFIXTAC =
     CT_cofixtac of ct_ID * ct_FORMULA
 and ct_COFIX_REC =
-    CT_cofix_rec of ct_ID * ct_FORMULA * ct_FORMULA
+    CT_cofix_rec of ct_ID * ct_BINDER_LIST * ct_FORMULA * ct_FORMULA
 and ct_COFIX_REC_LIST =
     CT_cofix_rec_list of ct_COFIX_REC * ct_COFIX_REC list
 and ct_COFIX_TAC_LIST =
@@ -276,7 +276,8 @@ and ct_FIX_BINDER =
 and ct_FIX_BINDER_LIST =
     CT_fix_binder_list of ct_FIX_BINDER * ct_FIX_BINDER list
 and ct_FIX_REC =
-    CT_fix_rec of ct_ID * ct_BINDER_NE_LIST * ct_ID_OPT * ct_FORMULA * ct_FORMULA
+    CT_fix_rec of ct_ID * ct_BINDER_NE_LIST * ct_ID_OPT *
+      ct_FORMULA * ct_FORMULA
 and ct_FIX_REC_LIST =
     CT_fix_rec_list of ct_FIX_REC * ct_FIX_REC list
 and ct_FIX_TAC_LIST =
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 8ff97b0c75..ff41852380 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -84,11 +84,12 @@ and fCOFIXTAC = function
    fFORMULA x2;
    fNODE "cofixtac" 2
 and fCOFIX_REC = function
-| CT_cofix_rec(x1, x2, x3) ->
+| CT_cofix_rec(x1, x2, x3, x4) ->
    fID x1;
-   fFORMULA x2;
+   fBINDER_LIST x2;
    fFORMULA x3;
-   fNODE "cofix_rec" 3
+   fFORMULA x4;
+   fNODE "cofix_rec" 4
 and fCOFIX_REC_LIST = function
 | CT_cofix_rec_list(x,l) ->
    fCOFIX_REC x;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 33b3488dbf..fad049a06b 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -293,22 +293,12 @@ let rec decompose_last = function
   | [a] -> [], a
   | a::tl -> let rl, b = decompose_last tl in (a::rl), b;;
 
-(* The boolean argument should be false if a name is not really necessary, 
-   for instance if there is only one argument.  On the other hand, all
-   recursive calls in this function should have the boolean argument to true,
-   because recursive calls mean that there is more than one argument. *)
-
-let rec make_fix_struct b = function
-    0, CProdN(_, [(na::tl,_)], CProdN(_, _,_)) -> xlate_id_opt na
-  | 0, CProdN(_, [([na],_)], _) ->
-      if b then xlate_id_opt na else ctv_ID_OPT_NONE
-  | n, CProdN(_, [(l,_)],body) -> 
-      let len = List.length l in
-	if len <= n then
-	  make_fix_struct true (n-len, body)
-	else
-	  xlate_id_opt(List.nth l n)
-  | _, _ -> xlate_error "unexpected result of parsing for Fixpoint";;
+let make_fix_struct (n,bl) =
+  let names = names_of_local_assums bl in
+  let nn = List.length names in
+  if nn = 1 then ctv_ID_OPT_NONE
+  else if n < nn then xlate_id_opt(List.nth names n)
+  else xlate_error "unexpected result of parsing for Fixpoint";;
 
 
 let rec xlate_binder = function
@@ -344,8 +334,6 @@ and
 and 
   xlate_binder_list = function
   l -> CT_binder_list( List.map xlate_binder_l l)
-and  cvt_fixpoint_binders bl =
-  CT_binder_list(List.map xlate_binder bl)
 and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 
      CRef r -> varc (xlate_reference r)
@@ -432,20 +420,22 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
        xlate_error "Second order variable not supported"
    | CEvar (_, _) -> xlate_error "CEvar not supported"
    | CCoFix (_, (_, id), lm::lmi) -> 
-     let strip_mutcorec (fid, arf, ardef) =
-	CT_cofix_rec (xlate_ident fid, xlate_formula arf, xlate_formula ardef) in
+     let strip_mutcorec (fid, bl,arf, ardef) =
+	CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
+                      xlate_formula arf, xlate_formula ardef) in
         CT_cofixc(xlate_ident id,
 	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
    | CFix (_, (_, id), lm::lmi) ->       
-     let strip_mutrec (fid, n, optional_nargs, arf, ardef) =
-       let struct_arg = make_fix_struct false (n, arf) in
-       let split_rank = match optional_nargs with
-	   Some v -> v
-	 | None -> n+1 in
-        let (bl,arf,ardef) = Ppconstr.split_fix split_rank arf ardef in
+     let strip_mutrec (fid, n, bl, arf, ardef) =
+        let (struct_arg,bl,arf,ardef) =
+         if bl = [] then
+           let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
+           let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
+           (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
+         else (make_fix_struct (n, bl),bl,arf,ardef) in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
-	match cvt_fixpoint_binders bl with
+	match xlate_binder_list bl with
 	  | CT_binder_list (b :: bl) ->
 	      CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
 			  struct_arg, arf, ardef)
@@ -1868,15 +1858,16 @@ let rec xlate_vernac =
 	  (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
    | VernacFixpoint [] -> xlate_error "mutual recursive"
    | VernacFixpoint (lm :: lmi) ->
-      let strip_mutrec ((fid, n, optional_nargs, arf, ardef), ntn) =
-	let struct_arg = make_fix_struct false (n, arf) in
-	let split_rank = match optional_nargs with
-	    Some v -> v
-	  | None -> n+1 in
-        let (bl,arf,ardef) = Ppconstr.split_fix split_rank arf ardef in
+      let strip_mutrec ((fid, n, bl, arf, ardef), ntn) =
+        let (struct_arg,bl,arf,ardef) =
+         if bl = [] then
+           let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
+           let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
+           (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
+         else (make_fix_struct (n, bl),bl,arf,ardef) in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
-	match cvt_fixpoint_binders bl with
+	match xlate_binder_list bl with
 	  | CT_binder_list (b :: bl) ->
 	      CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl), 
 			  struct_arg, arf, ardef)
@@ -1885,8 +1876,9 @@ let rec xlate_vernac =
 	  (CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))
    | VernacCoFixpoint [] -> xlate_error "mutual corecursive"
    | VernacCoFixpoint (lm :: lmi) ->
-      let strip_mutcorec (fid, arf, ardef) =
-	CT_cofix_rec (xlate_ident fid, xlate_formula arf, xlate_formula ardef) in
+      let strip_mutcorec (fid, bl, arf, ardef) =
+	CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
+                      xlate_formula arf, xlate_formula ardef) in
         CT_cofix_decl
 	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi))
    | VernacScheme [] -> xlate_error "induction scheme"
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fa1faf9cf3..0f0968aad7 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1009,14 +1009,16 @@ 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) ->
+      List.iter2 (fun (id1,i1,bl1,a1,b1) (id2,i2,bl2,a2,b2) ->
         if id1<>id2 || i1<>i2 then failwith "not same fix";
+        check_same_fix_binder bl1 bl2;
         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) ->
+      List.iter2 (fun (id1,bl1,a1,b1) (id2,bl2,a2,b2) ->
         if id1<>id2 then failwith "not same fix";
+        check_same_fix_binder bl1 bl2;
         check_same_type a1 a2;
         check_same_type b1 b2)
         fl1 fl2
@@ -1066,6 +1068,15 @@ and check_same_binder (nal1,e1) (nal2,e2) =
     if na1<>na2 then failwith "not same name") nal1 nal2;
   check_same_type e1 e2
 
+and check_same_fix_binder bl1 bl2 =
+  List.iter2 (fun b1 b2 ->
+    match b1,b2 with
+        LocalRawAssum(nal1,ty1), LocalRawAssum(nal2,ty2) ->
+          check_same_binder (nal1,ty1) (nal2,ty2)
+      | LocalRawDef(na1,def1), LocalRawDef(na2,def2) ->
+          check_same_binder ([na1],def1) ([na2],def2)          
+      | _ -> failwith "not same binder") bl1 bl2
+
 let same c d = try check_same_type c d; true with _ -> false
 
 (**********************************************************************)
@@ -1502,21 +1513,27 @@ let rec extern inctx scopes vars r =
         (Some na,option_app (extern_type scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars b1, sub_extern false scopes vars b2)
 
-  | RRec (loc,fk,idv,tyv,bv) ->
+  | RRec (loc,fk,idv,blv,tyv,bv) ->
       let vars' = Array.fold_right Idset.add idv vars in
       (match fk with
 	 | RFix (nv,n) ->
 	     let listdecl = 
 	       Array.mapi (fun i fi ->
-		 (fi,nv.(i), None, extern_type scopes vars tyv.(i),
-                  extern false scopes vars' bv.(i))) idv
+                 let (ids,bl) = extern_local_binder scopes vars blv.(i) in
+                 let vars0 = List.fold_right (name_fold Idset.add) ids vars in
+                 let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
+		 (fi,nv.(i), bl, extern_type scopes vars1 tyv.(i),
+                  extern false scopes vars0 bv.(i))) idv
 	     in 
 	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
 	 | RCoFix n -> 
 	     let listdecl =
                Array.mapi (fun i fi ->
-		 (fi,extern_type scopes vars tyv.(i),
-                  sub_extern false scopes vars' bv.(i))) idv
+                 let (ids,bl) = extern_local_binder scopes vars blv.(i) in
+                 let vars0 = List.fold_right (name_fold Idset.add) ids vars in
+                 let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
+		 (fi,bl,extern_type scopes vars1 tyv.(i),
+                  sub_extern false scopes vars0 bv.(i))) idv
 	     in
 	     CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
 
@@ -1557,6 +1574,29 @@ and factorize_lambda inctx scopes vars aty = function
            ((loc,na)::nal,c)
   | c -> ([],sub_extern inctx scopes vars c)
 
+and extern_local_binder scopes vars = function
+    [] -> ([],[])
+  | (na,Some bd,ty)::l ->
+      let na = name_app translate_ident na in
+      let (ids,l) =
+        extern_local_binder scopes (name_fold Idset.add na vars) l in
+      (na::ids,
+       LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l)
+      
+  | (na,None,ty)::l ->
+      let na = name_app translate_ident na in
+      let ty = extern_type scopes vars (anonymize_if_reserved na ty) in
+      (match extern_local_binder scopes (name_fold Idset.add na vars) l with
+          (ids,LocalRawAssum(nal,ty')::l)
+            when same ty ty' &
+              match na with Name id -> not (occur_var_constr_expr id ty')
+                | _ -> true ->
+              (na::ids,
+               LocalRawAssum((dummy_loc,na)::nal,ty')::l)
+        | (ids,l) ->
+            (na::ids,
+             LocalRawAssum([(dummy_loc,na)],ty) :: l))
+
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl,
    extern inctx scopes vars c)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a12df82f5b..0812baaac5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -530,18 +530,6 @@ let rec intern_cases_pattern scopes aliases tmp_scope = function
 (**********************************************************************)
 (* Fix and CoFix                                                      *)
 
-let rec intern_fix = function
-  | [] -> ([],[],[],[])
-  | (fi, n, on, c, t)::rest->
-      let (lf,ln,lc,lt) = intern_fix rest in
-      (fi::lf, n::ln, c::lc, t::lt)
-
-let rec intern_cofix = function
-  | [] -> ([],[],[])
-  | (fi, c, t)::rest -> 
-      let (lf,lc,lt) = intern_cofix rest in
-      (fi::lf, c::lc, t::lt)
-
 (**********************************************************************)
 (* Utilities for binders                                              *)
 
@@ -688,8 +676,9 @@ let internalise sigma env allow_soapp lvar c =
 	(match intern_impargs c env imp subscopes l with
           | [] -> c
           | l -> RApp (constr_loc x, c, l))
-    | CFix (loc, (locid,iddef), ldecl) ->
-	let (lf,ln,lc,lt) = intern_fix ldecl in
+    | CFix (loc, (locid,iddef), dl) ->
+        let lf = List.map (fun (id,_,_,_,_) -> id) dl in
+        let dl = Array.of_list dl in
 	let n =
 	  try
 	    (list_index iddef lf) -1
@@ -697,12 +686,22 @@ let internalise sigma env allow_soapp lvar c =
 	    raise (InternalisationError (locid,UnboundFixName (false,iddef)))
 	in
 	let ids' = List.fold_right Idset.add lf ids in
-	let defl =
-	  Array.of_list (List.map (intern (ids',None,scopes)) lt) in
-	let arityl = Array.of_list (List.map (intern_type env) lc) in
-	RRec (loc,RFix (Array.of_list ln,n), Array.of_list lf, arityl, defl)
-    | CCoFix (loc, (locid,iddef), ldecl) ->
-	let (lf,lc,lt) = intern_cofix ldecl in
+        let idl = Array.map
+          (fun (id,n,bl,ty,bd) ->
+            let ((ids'',_,_),rbl) =
+              List.fold_left intern_local_binder (env,[]) bl in
+	    let ids''' = List.fold_right Idset.add lf ids'' in
+            (List.rev rbl,
+             intern_type (ids'',tmp_scope,scopes) ty,
+             intern (ids''',None,scopes) bd)) dl in
+	RRec (loc,RFix (Array.map (fun (_,n,_,_,_) -> n) dl,n),
+              Array.of_list lf,
+              Array.map (fun (bl,_,_) -> bl) idl,
+              Array.map (fun (_,ty,_) -> ty) idl,
+              Array.map (fun (_,_,bd) -> bd) idl)
+    | CCoFix (loc, (locid,iddef), dl) ->
+        let lf = List.map (fun (id,_,_,_) -> id) dl in
+        let dl = Array.of_list dl in
 	let n =
           try 
 	    (list_index iddef lf) -1
@@ -710,10 +709,19 @@ let internalise sigma env allow_soapp lvar c =
 	    raise (InternalisationError (locid,UnboundFixName (true,iddef)))
 	in
 	let ids' = List.fold_right Idset.add lf ids in
-	let defl =
-	  Array.of_list (List.map (intern (ids',None,scopes)) lt) in
-	let arityl = Array.of_list (List.map (intern_type env) lc) in
-	RRec (loc,RCoFix n, Array.of_list lf, arityl, defl)
+        let idl = Array.map
+          (fun (id,bl,ty,bd) ->
+            let ((ids'',_,_),rbl) =
+              List.fold_left intern_local_binder (env,[]) bl in
+	    let ids''' = List.fold_right Idset.add lf ids'' in
+            (List.rev rbl,
+             intern_type (ids'',tmp_scope,scopes) ty,
+             intern (ids''',None,scopes) bd)) dl in
+	RRec (loc,RCoFix n,
+              Array.of_list lf,
+              Array.map (fun (bl,_,_) -> bl) idl,
+              Array.map (fun (_,ty,_) -> ty) idl,
+              Array.map (fun (_,_,bd) -> bd) idl)
     | CArrow (loc,c1,c2) ->
         RProd (loc, Anonymous, intern_type env c1, intern_type env c2)
     | CProdN (loc,[],c2) ->
@@ -813,6 +821,17 @@ let internalise sigma env allow_soapp lvar c =
   and intern_type (ids,_,scopes) =
     intern (ids,Some Symbols.type_scope,scopes)
 
+  and intern_local_binder ((ids,ts,sc as env),bl) = function
+      LocalRawAssum(nal,ty) ->
+        let ids' = List.fold_left
+          (fun ids (_,na) -> name_fold Idset.add na ids) ids nal in
+        ((ids',ts,sc),
+         List.map (fun (_,na) ->
+           (na,None,intern_type env ty)) nal @bl)
+    | LocalRawDef((loc,na),def) ->
+        ((name_fold Idset.add na ids,ts,sc),
+         (na,Some(intern env def),RHole(loc,BinderType na))::bl)
+
   and intern_eqn n (ids,tmp_scope,scopes as env) (loc,lhs,rhs) =
 	let (idsl_substl_list,pl) =
 	  List.split 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index ed4cdba39f..8334922741 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -69,8 +69,13 @@ let rec unloc = function
       RLetTuple (dummy_loc,nal,(na,option_app unloc po),unloc b,unloc c)
   | RIf (_,c,(na,po),b1,b2) ->
       RIf (dummy_loc,unloc c,(na,option_app unloc po),unloc b1,unloc b2)
-  | RRec (_,fk,idl,tyl,bv) ->
-      RRec (dummy_loc,fk,idl,Array.map unloc tyl,Array.map unloc bv)
+  | RRec (_,fk,idl,bl,tyl,bv) ->
+      RRec (dummy_loc,fk,idl,
+            Array.map (List.map 
+              (fun (na,obd,ty) -> (na,option_app unloc obd, unloc ty)))
+              bl,
+            Array.map unloc tyl,
+            Array.map unloc bv)
   | RCast (_,c,t) -> RCast (dummy_loc,unloc c,unloc t)
   | RSort (_,x) -> RSort (dummy_loc,x)
   | RHole (_,x)  -> RHole (dummy_loc,x)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 3d26e9d7f8..1fe8edaca3 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -361,22 +361,27 @@ type constr_expr =
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
-and fixpoint_expr = identifier * int * int option * constr_expr * constr_expr
+and fixpoint_expr =
+    identifier * int * local_binder list * constr_expr * constr_expr
 
-and cofixpoint_expr = identifier * constr_expr * constr_expr
+and local_binder =
+  | LocalRawDef of name located * constr_expr
+  | LocalRawAssum of name located list * constr_expr
+
+and cofixpoint_expr =
+    identifier * local_binder list * constr_expr * constr_expr
 
 (***********************)
 (* For binders parsing *)
 
-type local_binder =
-  | LocalRawDef of name located * constr_expr
-  | LocalRawAssum of name located list * constr_expr
-
 let rec local_binders_length = function
   | [] -> 0
   | LocalRawDef _::bl -> 1 + local_binders_length bl
   | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl
 
+let names_of_local_assums bl =
+  List.flatten (List.map (function LocalRawAssum(l,_)->l|_->[]) bl)
+
 (**********************************************************************)
 (* Functions on constr_expr *)
 
@@ -475,8 +480,19 @@ let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
 
 let map_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
-  let h (nal,t) (e,bl) = (map_binder g e nal,(nal,f e t)::bl) in
-  List.fold_right h bl (e,[])
+  let h (e,bl) (nal,t) = (map_binder g e nal,(nal,f e t)::bl) in
+  let (e,rbl) = List.fold_left h (e,[]) bl in
+  (e, List.rev rbl)
+
+let map_local_binders f g e bl =
+  (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
+  let h (e,bl) = function
+      LocalRawAssum(nal,ty) ->
+        (map_binder g e nal, LocalRawAssum(nal,f e ty)::bl)
+    | LocalRawDef((loc,na),ty) ->
+        (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) in
+  let (e,rbl) = List.fold_left h (e,[]) bl in
+  (e, List.rev rbl)
 
 let map_constr_expr_with_binders f g e = function
   | CArrow (loc,a,b) -> CArrow (loc,f e a,f e b)
@@ -518,9 +534,20 @@ let map_constr_expr_with_binders f g e = function
       let e' = option_fold_right (name_fold g) ona e in
       CIf (loc,f e c,(ona,option_app (f e') po),f e b1,f e b2)
   | CFix (loc,id,dl) ->
-      CFix (loc,id,List.map (fun (id,n,on,t,d) -> (id,n,on,f e t,f e d)) dl)
+      CFix (loc,id,List.map (fun (id,n,bl,t,d) -> 
+        let (e',bl') = map_local_binders f g e bl in
+        let t' = f e' t in
+        (* Note: fix names should be inserted before the arguments... *)
+        let e'' = List.fold_left (fun e (id,_,_,_,_) -> g id e) e' dl in
+        let d' = f e'' d in
+        (id,n,bl',t',d')) dl)
   | CCoFix (loc,id,dl) ->
-      CCoFix (loc,id,List.map (fun (id,t,d) -> (id,f e t,f e d)) dl)
+      CCoFix (loc,id,List.map (fun (id,bl,t,d) ->
+        let (e',bl') = map_local_binders f g e bl in
+        let t' = f e' t in
+        let e'' = List.fold_left (fun e (id,_,_,_) -> g id e) e' dl in
+        let d' = f e'' d in
+        (id,bl',t',d')) dl)
 
 (* Used in constrintern *)
 let rec replace_vars_constr_expr l = function
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index d35418b515..a56a96dea6 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -107,9 +107,16 @@ type constr_expr =
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
-and fixpoint_expr = identifier * int * int option * constr_expr * constr_expr
+and fixpoint_expr =
+    identifier * int * local_binder list * constr_expr * constr_expr
+
+and cofixpoint_expr =
+    identifier * local_binder list * constr_expr * constr_expr
+
+and local_binder =
+  | LocalRawDef of name located * constr_expr
+  | LocalRawAssum of name located list * constr_expr
 
-and cofixpoint_expr = identifier * constr_expr * constr_expr
 
 val constr_loc : constr_expr -> loc
 
@@ -131,6 +138,14 @@ val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
 val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
 val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
 
+(* For binders parsing *)
+
+(* Includes let binders *)
+val local_binders_length : local_binder list -> int
+
+(* Does not take let binders into account *)
+val names_of_local_assums : local_binder list -> name located list
+
 (* Used in correctness and interface; absence of var capture not guaranteed *)
 (* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
 
@@ -138,14 +153,6 @@ val map_constr_expr_with_binders :
   ('a -> constr_expr -> constr_expr) ->
       (identifier -> 'a -> 'a) -> 'a -> constr_expr -> constr_expr
 
-(* For binders parsing *)
-
-type local_binder =
-  | LocalRawDef of name located * constr_expr
-  | LocalRawAssum of name located list * constr_expr
-
-val local_binders_length : local_binder list -> int
-
 (* Concrete syntax for modules and modules types *)
 
 type with_declaration_ast = 
diff --git a/lib/util.ml b/lib/util.ml
index f57b9a6dbc..f2af9f6d43 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -401,6 +401,25 @@ let array_for_all2 f v1 v2 =
   let lv1 = Array.length v1 in
   lv1 = Array.length v2 && allrec (pred lv1) 
 
+let array_for_all3 f v1 v2 v3 =
+  let rec allrec = function
+    | -1 -> true
+    | n -> (f v1.(n) v2.(n) v3.(n)) && (allrec (n-1))
+  in 
+  let lv1 = Array.length v1 in
+  lv1 = Array.length v2 && lv1 = Array.length v3 && allrec (pred lv1) 
+
+let array_for_all4 f v1 v2 v3 v4 =
+  let rec allrec = function
+    | -1 -> true
+    | n -> (f v1.(n) v2.(n) v3.(n) v4.(n)) && (allrec (n-1))
+  in 
+  let lv1 = Array.length v1 in
+  lv1 = Array.length v2 &&
+  lv1 = Array.length v3 &&
+  lv1 = Array.length v4 &&
+    allrec (pred lv1) 
+
 let array_hd v = 
   match Array.length v with
     | 0 -> failwith "array_hd"
diff --git a/lib/util.mli b/lib/util.mli
index e2e46f5286..121b114a7d 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -136,6 +136,10 @@ val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
 val array_exists : ('a -> bool) -> 'a array -> bool
 val array_for_all : ('a -> bool) -> 'a array -> bool
 val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
+val array_for_all3 : ('a -> 'b -> 'c -> bool) ->
+  'a array -> 'b array -> 'c array -> bool
+val array_for_all4 : ('a -> 'b -> 'c -> 'd -> bool) ->
+  'a array -> 'b array -> 'c array -> 'd array -> bool
 val array_hd : 'a array -> 'a
 val array_tl : 'a array -> 'a array
 val array_last : 'a array -> 'a
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 27f52e73a1..c8f167eb3b 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -237,9 +237,19 @@ let subst_constr_expr a loc subs =
       let na = option_app (name_app (subst_id subs)) na in
       CIf (loc,subst c,(na,option_app subst po),subst b1,subst b2)
   | CFix (_,id,dl) ->
-      CFix (loc,id,List.map (fun (id,n,on, t,d) -> (id,n, on,subst t,subst d)) dl)
+      CFix (loc,id,List.map (fun (id,n,bl, t,d) ->
+        (id,n,
+         List.map(function
+             LocalRawAssum(nal,ty) -> LocalRawAssum(nal,subst ty)
+           | LocalRawDef(na,def) -> LocalRawDef(na,subst def)) bl,
+         subst t,subst d)) dl)
   | CCoFix (_,id,dl) ->
-      CCoFix (loc,id,List.map (fun (id,t,d) -> (id,subst t,subst d)) dl)
+      CCoFix (loc,id,List.map (fun (id,bl,t,d) ->
+        (id,
+         List.map(function
+             LocalRawAssum(nal,ty) -> LocalRawAssum(nal,subst ty)
+           | LocalRawDef(na,def) -> LocalRawDef(na,subst def)) bl,
+         subst t,subst d)) dl)
   in subst a
 
 let make_rule univ assoc etyp rule =
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3e513f0719..2f606ffd30 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -339,21 +339,19 @@ GEXTEND Gram
   fixbinder:
     [ [ id = base_ident; "/"; recarg = natural; ":"; type_ = constr;
         ":="; def = constr ->
-          (id, recarg-1, None, type_, def)
+          (id, recarg-1, [], type_, def)
       | id = base_ident; bl = ne_simple_binders_list; ":"; type_ = constr;
 	":="; def = constr ->
           let ni = List.length (List.flatten (List.map fst bl)) -1 in
-          let loc0 = fst (List.hd (fst (List.hd bl))) in
-          let loc1 = join_loc loc0 (constr_loc type_) in
-          let loc2 = join_loc loc0 (constr_loc def) in
-	  (id, ni, None, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)) ] ]
+          let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
+	  (id, ni, bl, type_, def) ] ]
   ;
   fixbinders:
     [ [ fbs = LIST1 fixbinder SEP "with" -> fbs ] ]
   ;
   cofixbinder:
     [ [ id = base_ident; ":"; type_ = constr; ":="; def = constr ->
-          (id, type_, def) ] ]
+          (id, [],type_, def) ] ]
   ;
   cofixbinders:
     [ [ fbs = LIST1 cofixbinder SEP "with" -> fbs ] ]
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index fb770768a9..606949e5f9 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -68,37 +68,33 @@ let rec mkCLambdaN loc bll c =
   | [] -> c
   | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
 
-let rec decls_of_binders = function
-  | [] -> []
-  | LocalRawDef _::bl -> decls_of_binders bl
-  | LocalRawAssum (idl,_)::bl -> idl @ decls_of_binders bl
-
-let rec index_of_annot bl ann =
-  match decls_of_binders bl,ann with
+let rec index_of_annot loc bl ann =
+  match names_of_local_assums bl,ann with
     | [_], None -> 0
     | lids, Some x ->
         let ids = List.map snd lids in
         (try list_index (snd x) ids - 1
-        with Not_found -> error "no such fix variable")
-    | _ -> error "cannot guess decreasing argument of fix"
+        with Not_found ->
+          user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable"))
+    | _ -> user_err_loc(loc,"index_of_annot",
+      Pp.str "cannot guess decreasing argument of fix")
 
-let mk_fixb (loc,id,bl,ann,body,(tloc,tyc)) =
-  let n = index_of_annot bl ann in
-  let nargs = List.length (decls_of_binders bl) in
+let mk_fixb (id,bl,ann,body,(loc,tyc)) =
+  let n = index_of_annot (fst id) bl ann in
   let ty = match tyc with
-      None -> CHole tloc
-    | Some t -> mkCProdN loc bl t in
-  (snd id,n,Some nargs,ty,mkCLambdaN loc bl body)
+      Some ty -> ty
+    | None -> CHole loc in
+  (snd id,n,bl,ty,body)
 
-let mk_cofixb (loc,id,bl,ann,body,(tloc,tyc)) =
+let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let _ = option_app (fun (aloc,_) ->
     Util.user_err_loc
       (aloc,"Constr:mk_cofixb",
        Pp.str"Annotation forbidden in cofix expression")) ann in
   let ty = match tyc with
-      None -> CHole tloc
-    | Some t -> mkCProdN loc bl t in
-  (snd id,ty,mkCLambdaN loc bl body)
+      Some ty -> ty
+    | None -> CHole loc in
+  (snd id,bl,ty,body)
 
 let mk_fix(loc,kw,id,dcls) =
   if kw then 
@@ -109,7 +105,7 @@ let mk_fix(loc,kw,id,dcls) =
     CCoFix(loc,id,fb)
 
 let mk_single_fix (loc,kw,dcl) =
-  let (_,id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl])
+  let (id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl])
 
 let binder_constr =
   create_constr_entry (get_univ "constr") "binder_constr"
@@ -255,7 +251,7 @@ GEXTEND Gram
   ;
   fix_decl:
     [ [ id=identref; bl=LIST0 binder_let; ann=fixannot; ty=type_cstr; ":=";
-        c=operconstr LEVEL "200" -> (loc,id,bl,ann,c,ty) ] ]
+        c=operconstr LEVEL "200" -> (id,bl,ann,c,ty) ] ]
   ;
   fixannot:
     [ [ "{"; IDENT "struct"; id=name; "}" -> Some id
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index def4b9fbf9..cde9061b3d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -252,17 +252,15 @@ GEXTEND Gram
     [ [ id = base_ident; bl = ne_fix_binders; ":"; type_ = constr;
         ":="; def = constr; ntn = OPT decl_notation ->
           let ni = List.length (List.flatten (List.map fst bl)) - 1 in
-          let loc0 = fst (List.hd (fst (List.hd bl))) in
-          let loc1 = join_loc loc0 (constr_loc type_) in
-          let loc2 = join_loc loc0 (constr_loc def) in
-	  ((id, ni, None, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)), ntn) ] ]
+          let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
+	  ((id, ni, bl, type_, def), ntn) ] ]
   ;
   specifrec:
     [ [ l = LIST1 onerec SEP "with" -> l ] ]
   ;
   onecorec:
     [ [ id = base_ident; ":"; c = constr; ":="; def = constr ->
-          (id,c,def) ] ]
+          (id,[],c,def) ] ]
   ;
   specifcorec:
     [ [ l = LIST1 onecorec SEP "with" -> l ] ]
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 70235d9ecf..75222eaa43 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -204,8 +204,7 @@ GEXTEND Gram
     [ [ id = base_ident; bl = LIST1 binder_let;
         annot = OPT rec_annotation; type_ = type_cstr; 
 	":="; def = lconstr; ntn = decl_notation ->
-          let names = List.map snd (G_constrnew.decls_of_binders bl) in
-	  let nargs = List.length names in
+          let names = List.map snd (names_of_local_assums bl) in
           let ni =
             match annot with
                 Some id ->
@@ -219,17 +218,12 @@ GEXTEND Gram
                       (loc,"Fixpoint",
                        Pp.str "the recursive argument needs to be specified");
                   0 in
-          let loc0 = G_constrnew.loc_of_binder_let bl in
-          let loc1 = join_loc loc0 (constr_loc type_) in
-          let loc2 = join_loc loc0 (constr_loc def) in
-	  ((id, ni, Some nargs, G_constrnew.mkCProdN loc1 bl type_,
-	    G_constrnew.mkCLambdaN loc2 bl def),ntn) ] ]
+	  ((id, ni, bl, type_, def),ntn) ] ]
   ;
   corec_definition:
     [ [ id = base_ident; bl = LIST0 binder_let; c = type_cstr; ":=";
         def = lconstr ->
-          (id,G_constrnew.mkCProdN loc bl c ,
-	   G_constrnew.mkCLambdaN loc bl def) ] ]
+          (id,bl,c ,def) ] ]
   ;
   rec_annotation:
     [ [ "{"; IDENT "struct"; id=IDENT; "}" -> id_of_string id ] ]
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 77853c5e1a..335d3b7964 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -110,6 +110,13 @@ let pr_binder pr (nal,t) =
 let pr_binders pr bl =
   hv 0 (prlist_with_sep pr_semicolon (pr_binder pr) bl)
 
+let pr_local_binder pr = function
+    LocalRawAssum(nal,t) -> pr_binder pr (nal,t)
+  | LocalRawDef((_,na),t) -> pr_let_binder pr na t
+
+let pr_local_binders pr bl =
+  hv 0 (prlist_with_sep pr_semicolon (pr_local_binder pr) bl)
+
 let pr_global vars ref = pr_global_env vars ref
 
 let rec pr_lambda_tail pr bll = function
@@ -155,13 +162,15 @@ let rec split_fix n typ def =
     let (bl,typ,def) = split_fix (n-1) typ def in
     (concat_binder na t bl,typ,def)
 
-let pr_fixdecl pr (id,n,_,t,c) =
-  let (bl,t,c) = split_fix (n+1) t c in
+let pr_fixdecl pr (id,n,bl,t,c) =
   pr_recursive_decl pr id 
-    (brk (1,2) ++ str "[" ++ pr_binders pr bl ++ str "]") t c
+    (brk (1,2) ++ str "[" ++ pr_local_binders pr bl ++ str "]") t c
 
-let pr_cofixdecl pr (id,t,c) =
-  pr_recursive_decl pr id (mt ()) t c
+let pr_cofixdecl pr (id,bl,t,c) =
+  let  b =
+    if bl=[] then mt() else
+      brk(1,2) ++ str"[" ++ pr_local_binders pr bl ++ str "]" in
+  pr_recursive_decl pr id b t c
 
 let pr_recursive fix pr_decl id = function
   | [] -> anomaly "(co)fixpoint with no definition"
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 0e8b84f741..8f00678f1e 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -95,6 +95,29 @@ let idopt_of_name = function
   | Name id -> Some id
   | Anonymous -> None
 
+let ast_of_binders bl =
+  List.map (fun (nal,isdef,ty) ->
+    if isdef then ope("LETBINDER",ty::List.map ast_of_name nal)
+    else ope("BINDER",ty::List.map ast_of_name nal)) bl
+
+let ast_type_of_binder bl t =
+  List.fold_right (fun (nal,isdef,ty) ast ->
+    if isdef then
+      ope("LETIN",[ty;slam(idopt_of_name (List.hd nal),ast)])
+    else
+      ope("PROD",[ty;List.fold_right
+        (fun na ast -> slam(idopt_of_name na,ast)) nal ast]))
+    bl t
+
+let ast_body_of_binder bl t =
+  List.fold_right (fun (nal,isdef,ty) ast ->
+    if isdef then
+      ope("LETIN",[ty;slam(idopt_of_name (List.hd nal),ast)])
+    else
+      ope("LAMBDA",[ty;List.fold_right
+        (fun na ast -> slam(idopt_of_name na,ast)) nal ast]))
+    bl t
+
 let ast_of_constant_ref sp =
   ope("CONST", [path_section dummy_loc sp])
 
@@ -259,12 +282,12 @@ let rec ast_of_raw = function
   | RLetTuple _ | RIf _ ->
       error "Let tuple not supported in v7"
 
-  | RRec (_,fk,idv,tyv,bv) ->
+  | RRec (_,fk,idv,blv,tyv,bv) ->
       let alfi = Array.map ast_of_ident idv in
       (match fk with
 	 | RFix (nv,n) ->
              let rec split_lambda binds = function
-	       | (0, t) -> (binds,ast_of_raw t)
+	       | (0, t) -> (List.rev binds,ast_of_raw t)
 	       | (n, RLetIn (_,na,b,c)) ->
 		   let bind = ope("LETBINDER",[ast_of_raw b;ast_of_name na]) in
 		   split_lambda (bind::binds) (n,c)
@@ -280,11 +303,26 @@ let rec ast_of_raw = function
 	     let listdecl = 
 	       Array.mapi
 		 (fun i fi ->
-		    let (lparams,astdef) = split_lambda [] (nv.(i)+1,bv.(i)) in
-		    let asttyp = split_product (nv.(i)+1,tyv.(i)) in
-		    ope("FDECL",
-		       	[fi; ope ("BINDERS",List.rev lparams); 
-			 asttyp; astdef]))
+                   if List.length blv.(i) >= nv.(i)+1 then
+                     let (oldfixp,factb) = list_chop (nv.(i)+1) blv.(i) in
+                     let bl = factorize_local_binder oldfixp in
+                     let factb = factorize_local_binder factb in
+                     let asttyp = ast_type_of_binder factb
+                       (ast_of_raw tyv.(i)) in
+                     let astdef = ast_body_of_binder factb
+                       (ast_of_raw bv.(i)) in
+                     ope("FDECL",[fi;ope("BINDERS",ast_of_binders bl);
+                                  asttyp; astdef])
+                   else
+                     let n = nv.(i)+1 - List.length blv.(i) in
+		     let (lparams,astdef) =
+                       split_lambda [] (n,bv.(i)) in
+                     let bl = factorize_local_binder blv.(i) in
+                     let lparams = ast_of_binders bl @ lparams in
+		     let asttyp = split_product (n,tyv.(i)) in
+		     ope("FDECL",
+		         [fi; ope ("BINDERS",lparams); 
+		          asttyp; astdef]))
 		 alfi
 	     in 
 	     ope("FIX", alfi.(n)::(Array.to_list listdecl))
@@ -292,7 +330,10 @@ let rec ast_of_raw = function
 	     let listdecl =
                Array.mapi 
 		 (fun i fi ->
-		    ope("CFDECL",[fi; ast_of_raw tyv.(i); ast_of_raw bv.(i)]))
+                   let bl = factorize_local_binder blv.(i) in
+                   let asttyp = ast_type_of_binder bl (ast_of_raw tyv.(i)) in
+                   let astdef = ast_body_of_binder bl (ast_of_raw bv.(i)) in
+		   ope("CFDECL",[fi; asttyp; astdef]))
 		 alfi
 	     in 
 	     ope("COFIX", alfi.(n)::(Array.to_list listdecl)))
@@ -325,6 +366,18 @@ and factorize_binder n oper na aty c =
   in
   (p,slam(idopt_of_name na, body))
 
+and factorize_local_binder = function
+    [] -> []
+  | (na,Some bd,ty)::l ->
+      ([na],true,ast_of_raw bd) :: factorize_local_binder l
+  | (na,None,ty)::l ->
+      let ty = ast_of_raw ty in
+      (match factorize_local_binder l with
+          (lna,false,ty') :: l when ty=ty' ->
+            (na::lna,false,ty') :: l
+        | l -> ([na],false,ty) :: l)
+
+
 let ast_of_rawconstr = ast_of_raw
 
 (******************************************************************)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ffd2fad54a..e1f0da13b5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -358,45 +358,14 @@ and detype_fix tenv avoid env (vn,_ as nvn) (names,tys,bodies) =
 	 let id = next_name_away na avoid in 
 	 (id::avoid, add_name (Name id) env, id::l))
       (avoid, env, []) names in
- (* Be sure that bodies and types share the same names *)
-  let rec share_names n l avoid env c t =
-    if n = 0 then
-      let c = detype tenv avoid env c in
-      let t = detype tenv avoid env t in
-      List.fold_left (fun (c,typ) (na,body,t) -> match body with
-	| None -> (RLambda (dummy_loc,na,t,c),RProd (dummy_loc,na,t,typ))
-	| Some b -> (RLetIn (dummy_loc,na,b,c),RLetIn (dummy_loc,na,b,typ)))
-	(c,t) l
-    else match kind_of_term c, kind_of_term t with
-      | Lambda (na,t,c), Prod (_,t',c') ->
-          let t = detype tenv avoid env t in
-	  let id = next_name_away na avoid in 
-          let avoid = id::avoid and env = add_name (Name id) env in
-          share_names (n-1) ((Name id,None,t)::l) avoid env c c'
-      (* May occur for fix built interactively *)
-      | LetIn (na,b,t',c), _ ->
-          let t' = detype tenv avoid env t' in
-          let b = detype tenv avoid env b in
-	  let id = next_name_away na avoid in 
-          let avoid = id::avoid and env = add_name (Name id) env in
-          share_names n ((Name id,Some b,t')::l) avoid env c t
-      (* Only if built with the f/n notation or w/o let-expansion in types *)
-      | _, LetIn (_,b,_,t) ->
-	  share_names n l avoid env c (subst1 b t)
-      (* If it is an open proof: we cheat and eta-expand *)
-      | _, Prod (na',t',c') ->
-          let t' = detype tenv avoid env t' in
-          let avoid = name_cons na' avoid and env = add_name na' env in
-          let appc = mkApp (lift 1 c,[|mkRel 1|]) in
-          share_names (n-1) ((na',None,t')::l) avoid env appc c'
-      (* If built with the f/n notation: we renounce to share names *)
-      | _ -> share_names 0 l avoid env c t in
   let n = Array.length tys in
   let v = array_map3
-    (fun c t i -> share_names (i+1) [] def_avoid def_env c (lift n t))
+    (fun c t i -> share_names tenv (i+1) [] def_avoid def_env c (lift n t))
     bodies tys vn in
   RRec(dummy_loc,RFix nvn,Array.of_list (List.rev lfi),
-       Array.map snd v, Array.map fst v)
+       Array.map (fun (bl,_,_) -> bl) v,
+       Array.map (fun (_,_,ty) -> ty) v,
+       Array.map (fun (_,bd,_) -> bd) v)
 
 and detype_cofix tenv avoid env n (names,tys,bodies) =
   let def_avoid, def_env, lfi =
@@ -405,9 +374,53 @@ and detype_cofix tenv avoid env n (names,tys,bodies) =
 	 let id = next_name_away na avoid in 
 	 (id::avoid, add_name (Name id) env, id::l))
       (avoid, env, []) names in
+  let n = Array.length tys in
+  let v = array_map2
+    (fun c t -> share_names tenv 0 [] def_avoid def_env c (lift n t))
+    bodies tys in
   RRec(dummy_loc,RCoFix n,Array.of_list (List.rev lfi),
-       Array.map (detype tenv avoid env) tys,
-       Array.map (detype tenv def_avoid def_env) bodies)
+       Array.map (fun (bl,_,_) -> bl) v,
+       Array.map (fun (_,_,ty) -> ty) v,
+       Array.map (fun (_,bd,_) -> bd) v)
+
+and share_names tenv n l avoid env c t =
+  if !Options.v7 && n=0 then
+    let c = detype tenv avoid env c in
+    let t = detype tenv avoid env t in
+    (l,c,t)
+  else
+  match kind_of_term c, kind_of_term t with
+    | Lambda (na,t,c), Prod (na',t',c') ->
+        let na = match (na,na') with
+            Name _, _ -> na
+          | _, Name _ -> na'
+          | _ -> na in 
+        let t = detype tenv avoid env t in
+	let id = next_name_away na avoid in 
+        let avoid = id::avoid and env = add_name (Name id) env in
+        share_names tenv (n-1) ((Name id,None,t)::l) avoid env c c'
+    (* May occur for fix built interactively *)
+    | LetIn (na,b,t',c), _ ->
+        let t' = detype tenv avoid env t' in
+        let b = detype tenv avoid env b in
+	let id = next_name_away na avoid in 
+        let avoid = id::avoid and env = add_name (Name id) env in
+        share_names tenv n ((Name id,Some b,t')::l) avoid env c t
+    (* Only if built with the f/n notation or w/o let-expansion in types *)
+    | _, LetIn (_,b,_,t) ->
+	share_names tenv n l avoid env c (subst1 b t)
+    (* If it is an open proof: we cheat and eta-expand *)
+    | _, Prod (na',t',c') ->
+        let t' = detype tenv avoid env t' in
+        let avoid = name_cons na' avoid and env = add_name na' env in
+        let appc = mkApp (lift 1 c,[|mkRel 1|]) in
+        share_names tenv (n-1) ((na',None,t')::l) avoid env appc c'
+    (* If built with the f/n notation: we renounce to share names *)
+    | _ ->
+        if n>0 then warning "Detyping.detype: cannot factorize fix enough";
+        let c = detype tenv avoid env c in
+        let t = detype tenv avoid env t in
+        (l,c,t)
 
 and detype_eqn tenv avoid env constr construct_nargs branch =
   let make_pat x avoid env b ids =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5f2d8d97dd..a2ea06e4ef 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -244,31 +244,54 @@ let rec pretype tycon env isevars lvar = function
 	     { uj_val = new_isevar isevars env (loc,k) ty; uj_type = ty }
 	 | None -> error_unsolvable_implicit loc env (evars_of isevars) k)
 
-  | RRec (loc,fixkind,names,lar,vdef) ->
+  | RRec (loc,fixkind,names,bl,lar,vdef) ->
+      let rec type_bl env ctxt = function
+          [] -> ctxt
+        | (na,None,ty)::bl ->
+            let ty' = pretype_type empty_valcon env isevars lvar ty in
+            let dcl = (na,None,ty'.utj_val) in
+            type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
+        | (na,Some bd,ty)::bl ->
+            let ty' = pretype_type empty_valcon env isevars lvar ty in
+            let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in
+            let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
+            type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
+      let ctxtv = Array.map (type_bl env empty_rel_context) bl in
       let larj =
-        Array.map (pretype_type empty_valcon env isevars lvar) lar in
+        array_map2
+          (fun e ar ->
+            pretype_type empty_valcon (push_rel_context e env) isevars lvar ar)
+          ctxtv lar in
       let lara = Array.map (fun a -> a.utj_val) larj in
+      let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
       let nbfix = Array.length lar in
       let names = Array.map (fun id -> Name id) names in
-      let newenv = push_rec_types (names,lara,[||]) env in
+      (* Note: bodies are not used by push_rec_types, so [||] is safe *)
+      let newenv = push_rec_types (names,ftys,[||]) env in
       let vdefj =
-	Array.mapi 
-	  (fun i def -> (* we lift nbfix times the type in tycon, because of
-			 * the nbfix variables pushed to newenv *)
-             pretype (mk_tycon (lift nbfix (larj.(i).utj_val)))
-               newenv isevars lvar def)
-          vdef in
-      evar_type_fixpoint loc env isevars names lara vdefj;
+	array_map2_i 
+	  (fun i ctxt def ->
+            (* we lift nbfix times the type in tycon, because of
+	     * the nbfix variables pushed to newenv *)
+            let (ctxt,ty) =
+              decompose_prod_n_assum (rel_context_length ctxt)
+                (lift nbfix ftys.(i)) in
+            let nenv = push_rel_context ctxt newenv in
+            let j = pretype (mk_tycon ty) nenv isevars lvar def in
+            { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
+              uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
+          ctxtv vdef in
+      evar_type_fixpoint loc env isevars names ftys vdefj;
       let fixj =
 	match fixkind with
 	  | RFix (vn,i as vni) ->
-	      let fix = (vni,(names,lara,Array.map j_val vdefj)) in
+	      let fix = (vni,(names,ftys,Array.map j_val vdefj)) in
 	      (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
-	      make_judge (mkFix fix) lara.(i)
+	      make_judge (mkFix fix) ftys.(i)
 	  | RCoFix i -> 
-	      let cofix = (i,(names,lara,Array.map j_val vdefj)) in
+	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
 	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
-	      make_judge (mkCoFix cofix) lara.(i) in
+	      make_judge (mkCoFix cofix) ftys.(i) in
       inh_conv_coerce_to_tycon loc env isevars fixj tycon
 
   | RSort (loc,s) ->
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 6442ca9693..6e7f8f70fc 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -70,19 +70,20 @@ type rawconstr =
   | RCases of loc * (rawconstr option * rawconstr option ref) *
       (rawconstr * (name * (loc * inductive * name list) option) ref) list * 
       (loc * identifier list * cases_pattern list * rawconstr) list
-      (* Rem: "ref" used for the v7->v8 translation only *)
   | ROrderedCase of loc * case_style * rawconstr option * rawconstr * 
       rawconstr array * rawconstr option ref
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
-  | RRec of loc * fix_kind * identifier array * 
+  | RRec of loc * fix_kind * identifier array * rawdecl list array *
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * hole_kind)
   | RCast of loc * rawconstr * rawconstr
   | RDynamic of loc * Dyn.t
 
+and rawdecl = name * rawconstr option * rawconstr
+
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,{contents=(na,None)}) -> [na]
@@ -97,6 +98,7 @@ let cases_predicate_names tml =
 
    - boolean in POldCase means it is recursive
 i*)
+let map_rawdecl f (na,obd,ty) = (na,option_app f obd,f ty)
 
 let map_rawconstr f = function
   | RVar (loc,id) -> RVar (loc,id)
@@ -114,9 +116,12 @@ let map_rawconstr f = function
       RLetTuple (loc,nal,(na,option_app f po),f b,f c)
   | RIf (loc,c,(na,po),b1,b2) ->
       RIf (loc,f c,(na,option_app f po),f b1,f b2)
-  | RRec (loc,fk,idl,tyl,bv) -> RRec (loc,fk,idl,Array.map f tyl,Array.map f bv)
+  | RRec (loc,fk,idl,bl,tyl,bv) ->
+      RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl,
+            Array.map f tyl,Array.map f bv)
   | RCast (loc,c,t) -> RCast (loc,f c,f t)
   | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
+  
 
 (*
 let name_app f e = function
@@ -176,9 +181,18 @@ let occur_rawconstr id =
         or (occur b) or (not (List.mem (Name id) nal) & (occur c))
     | RIf (loc,c,rtntyp,b1,b2) -> 
 	occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
-    | RRec (loc,fk,idl,tyl,bv) ->
-	(array_exists occur tyl) or
-	(not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv)
+    | RRec (loc,fk,idl,bl,tyl,bv) ->
+        not (array_for_all4 (fun fid bl ty bd ->
+          let rec occur_fix = function
+              [] -> not (occur ty) && (fid=id or not(occur bd))
+            | (na,bbd,bty)::bl ->
+                not (occur bty) &&
+                (match bbd with
+                    Some bd -> not (occur bd)
+                  | _ -> true) &&
+                (na=Name id or not(occur_fix bl)) in
+          occur_fix bl)
+          idl bl tyl bv)
     | RCast (loc,c,t) -> (occur c) or (occur t)
     | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false
 
@@ -275,11 +289,17 @@ let rec subst_raw subst raw =
 	if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else
           RIf (loc,c',(na,po'),b1',b2')
 
-  | RRec (loc,fix,ida,ra1,ra2) -> 
+  | RRec (loc,fix,ida,bl,ra1,ra2) -> 
       let ra1' = array_smartmap (subst_raw subst) ra1
       and ra2' = array_smartmap (subst_raw subst) ra2 in
-	if ra1' == ra1 && ra2' == ra2 then raw else
-	  RRec (loc,fix,ida,ra1',ra2')
+      let bl' = array_smartmap
+        (list_smartmap (fun (na,obd,ty as dcl) ->
+          let ty' = subst_raw subst ty in
+          let obd' = option_smartmap (subst_raw subst) obd in
+          if ty'==ty & obd'==obd then dcl else (na,obd',ty')))
+        bl in
+	if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
+	  RRec (loc,fix,ida,bl',ra1',ra2')
 
   | RSort _ -> raw
 
@@ -310,7 +330,7 @@ let loc_of_rawconstr = function
   | ROrderedCase (loc,_,_,_,_,_) -> loc
   | RLetTuple (loc,_,_,_,_) -> loc
   | RIf (loc,_,_,_,_) -> loc
-  | RRec (loc,_,_,_,_) -> loc
+  | RRec (loc,_,_,_,_,_) -> loc
   | RSort (loc,_) -> loc
   | RHole (loc,_) -> loc
   | RCast (loc,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 869861ccd7..e5b2a23fe8 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -73,13 +73,15 @@ type rawconstr =
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
-  | RRec of loc * fix_kind * identifier array * 
+  | RRec of loc * fix_kind * identifier array * rawdecl list array *
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * hole_kind)
   | RCast of loc * rawconstr * rawconstr
   | RDynamic of loc * Dyn.t
 
+and rawdecl = name * rawconstr option * rawconstr
+
 val cases_predicate_names : 
   (rawconstr * (name * (loc * inductive * name list) option) ref) list ->
       name list
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 14482cb7a1..5c792a463b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -242,12 +242,13 @@ let coerce_to_inductive = function
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 let atomic_mactab = ref Idmap.empty
 let add_primitive_tactic s tac =
-  let id = id_of_string s in
-  atomic_mactab := Idmap.add id tac !atomic_mactab
+  (if not !Options.v7 then
+    let id = id_of_string s in
+    atomic_mactab := Idmap.add id tac !atomic_mactab)
 
 let _ =
   if not !Options.v7 then
-    let nocl = {onhyps=Some[];onconcl=true; concl_occs=[]} in
+    (let nocl = {onhyps=Some[];onconcl=true; concl_occs=[]} in
     List.iter
       (fun (s,t) -> add_primitive_tactic s (TacAtom((0,0),t)))
       [ "red", TacReduce(Red false,nocl);
@@ -266,8 +267,14 @@ let _ =
         "constructor", TacAnyConstructor None;
         "reflexivity", TacReflexivity;
         "symmetry", TacSymmetry nocl
-      ]
-
+      ];
+    List.iter
+      (fun (s,t) -> add_primitive_tactic s t)
+      [ "idtac",TacId "";
+        "fail", TacFail(ArgArg 0,"");
+        "fresh", TacArg(TacFreshId None)
+      ])
+ 
 let lookup_atomic id = Idmap.find id !atomic_mactab
 let is_atomic id = Idmap.mem id !atomic_mactab
 let is_atomic_kn kn =
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
new file mode 100644
index 0000000000..270fff4ef2
--- /dev/null
+++ b/test-suite/output/Fixpoint.v
@@ -0,0 +1,7 @@
+Require PolyList.
+
+Check Fix F { F/4 : (A,B:Set)(A->B)->(list A)->(list B) :=
+ [_,_,f,l]Cases l of
+   nil => (nil ?)
+ | (cons a l) => (cons (f a) (F ? ? f l))
+ end}.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 46de560b46..30548d74d2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -456,7 +456,8 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)  =
   (* Declare the notations for the recursive types pushed in local context*)
   let (rec_sign,arityl) = 
     List.fold_left 
-      (fun (env,arl) ((recname,_,_,arityc,_),_) -> 
+      (fun (env,arl) ((recname,_,bl,arityc,_),_) -> 
+        let arityc = prod_rawconstr arityc bl in
         let arity = interp_type sigma env0 arityc in
         (Environ.push_named (recname,None,arity) env, (arity::arl)))
       (env0,[]) lnameargsardef in
@@ -479,7 +480,8 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)  =
 	      (Lib.cwd(),SectionLocalAssum arity, IsAssumption Definitional) in
 	    ()) lrecnames arityl;
 	List.map2
-	  (fun ((_,_,_,_,def),_) arity ->
+	  (fun ((_,_,bl,_,def),_) arity ->
+            let def = abstract_rawconstr def bl in
             interp_casted_constr sigma rec_sign def arity)
           lnameargsardef arityl
       with e ->
@@ -521,14 +523,15 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)  =
     Metasyntax.add_notation_interpretation df [] c scope) notations
 
 let build_corecursive lnameardef = 
-  let lrecnames = List.map (fun (f,_,_) -> f) lnameardef
+  let lrecnames = List.map (fun (f,_,_,_) -> f) lnameardef
   and sigma = Evd.empty
   and env0 = Global.env() in
   let fs = States.freeze() in
   let (rec_sign,arityl) = 
     try 
       List.fold_left 
-        (fun (env,arl) (recname,arityc,_) -> 
+        (fun (env,arl) (recname,bl,arityc,_) -> 
+           let arityc = prod_rawconstr arityc bl in
            let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in
 	   let arity = arj.utj_val in
            let _ = declare_variable recname
@@ -540,8 +543,10 @@ let build_corecursive lnameardef =
   let arityl = List.rev arityl in
   let recdef =
     try 
-      List.map (fun (_,arityc,def) ->
-		  let arity = interp_constr sigma rec_sign arityc in
+      List.map (fun (_,bl,arityc,def) ->
+        let arityc = prod_rawconstr arityc bl in
+        let def = abstract_rawconstr def bl in
+	let arity = interp_constr sigma rec_sign arityc in
                   interp_casted_constr sigma rec_sign def arity)
         lnameardef
     with e -> 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 8438e9b02b..f72c533e1e 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -154,7 +154,7 @@ let pr_new_syntax loc ocom =
   if !translate_file then
     msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
   else
-    msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ com));
+    msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
   States.unfreeze fs;
   Constrintern.set_temporary_implicits_in [];
   Constrextern.set_temporary_implicits_out [];
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index b98be6c6c7..2825344e45 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -76,7 +76,7 @@ let pr_notation pr s env =
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
 
-let surround p = str"(" ++ p ++ str")"
+let surround p = hov 1 (str"(" ++ p ++ str")")
 
 let pr_located pr ((b,e),x) =
   if Options.do_translate() && (b,e)<>dummy_loc then
@@ -350,24 +350,15 @@ let pr_recursive_decl pr id bl annot t c =
   pr_opt_type_spc pr t ++ str " :=" ++
   pr_sep_com (fun () -> 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,c,t) = extract_def_binders c0 t0 in
-  let (bl,t,c) =
-    let ids = List.flatten (List.map name_of_binder bl) in
-    if List.length ids <= n then split_fix (n+1) t0 c0 else (bl,t,c) in
+let pr_fixdecl pr (id,n,bl,t,c) =
   let annot =
-    let ids = List.flatten (List.map name_of_binder bl) in
+    let ids = names_of_local_assums bl in
     if List.length ids > 1 then 
       spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}"
     else mt() in
   pr_recursive_decl pr id bl annot t c
 
-let pr_cofixdecl pr (id,t,c) =
-  let (bl,c,t) = extract_def_binders c t in
+let pr_cofixdecl pr (id,bl,t,c) =
   pr_recursive_decl pr id bl (mt()) t c
 
 let pr_recursive pr_decl id = function
@@ -588,6 +579,20 @@ let rec pr sep inherited a =
 
 let pr = pr mt
 
+let rec abstract_constr_expr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
+      (abstract_constr_expr c bl)
+      
+let rec prod_constr_expr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> mkProdC([x],t,b)) idl
+      (prod_constr_expr c bl)
+
 let rec strip_context n iscast t =
   if n = 0 then
     [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t
@@ -619,12 +624,15 @@ let rec strip_context n iscast t =
 	LocalRawDef (na,b) :: bl', c
     | _ -> anomaly "ppconstrnew: strip_context"
 
-let transf istype env n iscast c =
+let transf istype env iscast bl c =
+  let c' =
+    if istype then abstract_constr_expr c bl 
+    else prod_constr_expr c bl in
   if Options.do_translate() then
     let r = 
       Constrintern.for_grammar
         (Constrintern.interp_rawconstr_gen istype Evd.empty env false ([],[]))
-	c in
+	c' in
     begin try
       (* Try to infer old case and type annotations *)
       let _ = Pretyping.understand_gen_tcc Evd.empty env [] None r in 
@@ -634,11 +642,12 @@ let transf istype env n iscast c =
       (if istype then Constrextern.extern_rawtype
       else Constrextern.extern_rawconstr)
       (Termops.vars_of_env env) r in
+    let n = local_binders_length bl in
     strip_context n iscast c
-  else [], c
+  else bl, c
 
-let pr_constr_env env c = pr lsimple (snd (transf false env 0 false c))
-let pr_lconstr_env env c = pr ltop (snd (transf false env 0 false c))
+let pr_constr_env env c = pr lsimple (snd (transf false env false [] c))
+let pr_lconstr_env env c = pr ltop (snd (transf false env false [] c))
 let pr_constr c = pr_constr_env (Global.env()) c
 let pr_lconstr c = pr_lconstr_env (Global.env()) c
 
@@ -658,10 +667,11 @@ let is_Eval_key c =
 let pr_protect_eval c =
   if is_Eval_key c then h 0 (str "(" ++ pr ltop c ++ str ")") else pr ltop c
 
-let pr_lconstr_env_n env n b c =
-  let bl, c = transf false env n b c in bl, pr_protect_eval c
-let pr_type_env_n env n c = pr ltop (snd (transf true env n false c))
-let pr_type c = pr ltop (snd (transf true (Global.env()) 0 false c))
+let pr_lconstr_env_n env iscast bl c =
+  let bl, c = transf false env iscast bl c in
+  bl, pr_protect_eval c
+let pr_type_env_n env bl c = pr ltop (snd (transf true env false bl c))
+let pr_type c = pr ltop (snd (transf true (Global.env()) false [] c))
 
 let transf_pattern env c =
   if Options.do_translate() then
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 542549f74e..2b79c6b71b 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -65,14 +65,17 @@ 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_env_n : env -> int -> bool -> constr_expr -> 
+val pr_lconstr_env_n : env -> bool -> local_binder list -> constr_expr -> 
   local_binder list * std_ppcmds
-val pr_type_env_n : env -> int -> constr_expr -> std_ppcmds
+val pr_type_env_n : env -> local_binder list -> constr_expr -> std_ppcmds
 val pr_type : constr_expr -> std_ppcmds
 val pr_cases_pattern : cases_pattern_expr -> std_ppcmds
 val pr_may_eval :
   ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval
     -> std_ppcmds
+val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
+val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
+
 
 val pr_rawconstr_env : env -> rawconstr -> std_ppcmds
 val pr_lrawconstr_env : env -> rawconstr -> std_ppcmds
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index cfeb12f06c..2fd54a006a 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -259,7 +259,8 @@ let pr_module_vardecls pr_c (idl,mty) =
       [make_mbid lib_dir (string_of_id id),
        Modintern.interp_modtype (Global.env()) mty]) idl;
   (* Builds the stream *)
-  spc() ++ str"(" ++ prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")"
+  spc() ++
+  hov 1 (str"(" ++ prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")
 
 let pr_module_binders l pr_c = 
   (* Effet de bord complexe pour garantir la declaration des noms des
@@ -275,7 +276,8 @@ let rec pr_module_expr = function
   | CMEapply (me1,(CMEident _ as me2)) ->
       pr_module_expr me1 ++ spc() ++ pr_module_expr me2
   | CMEapply (me1,me2) ->
-      pr_module_expr me1 ++ spc() ++ str"(" ++ pr_module_expr me2 ++ str")"
+      pr_module_expr me1 ++ spc() ++
+      hov 1 (str"(" ++ pr_module_expr me2 ++ str")")
 
 (*
 let pr_opt_casted_constr pr_c = function
@@ -285,7 +287,7 @@ let pr_opt_casted_constr pr_c = function
 
 let pr_type_option pr_c = function
   | CHole loc -> mt()
-  | _ as c -> str":" ++ pr_c c
+  | _ as c -> brk(0,2) ++ str":" ++ pr_c c
 
 let without_translation f x =
   let old = Options.do_translate () in
@@ -299,20 +301,6 @@ let pr_decl_notation prc =
     str "where " ++ qsnew ntn ++ str " := " ++ without_translation prc c ++
     pr_opt (fun sc -> str ": " ++ str sc) scopt)
 
-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)
-      
-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)
-
 let pr_vbinders l =
   hv 0 (pr_binders l)
 
@@ -320,9 +308,7 @@ let pr_binders_arg =
   pr_ne_sep spc pr_binders
 
 let pr_and_type_binders_arg bl =
-  let n = local_binders_length bl in
-  let c = abstract_rawconstr (CHole dummy_loc) bl in
-  let bl, _ = pr_lconstr_env_n (Global.env()) n false c in
+  let bl, _ = pr_lconstr_env_n (Global.env()) false bl (CHole dummy_loc) in
   pr_binders_arg bl
 
 let pr_onescheme (id,dep,ind,s) =
@@ -369,7 +355,8 @@ let pr_ne_params_list pr_c l =
   match factorize l with
     | [p] -> pr_params pr_c p
     | l ->
-	prlist_with_sep spc (fun p -> str "(" ++ pr_params pr_c p ++ str ")") l
+	prlist_with_sep spc
+          (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l
 (*
   prlist_with_sep pr_semicolon (pr_params pr_c)
 *)
@@ -403,7 +390,7 @@ let pr_syntax_modifier = function
 let pr_syntax_modifiers = function
   | [] -> mt()
   | l -> spc() ++ 
-      hov 0 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
+      hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
 
 let pr_grammar_tactic_rule (name,(s,pil),t) =
 (*
@@ -619,14 +606,10 @@ let rec pr_vernac = function
                   (bl2,CCast (dummy_loc,body,ty'),
                    spc() ++ str":" ++
                    pr_sep_com spc
-                     (pr_type_env_n (Global.env())
-                       (local_binders_length bl + local_binders_length bl2))
-                     (prod_rawconstr ty bl)) in
-	    let n = local_binders_length bl + local_binders_length bl2 in
+                     (pr_type_env_n (Global.env()) (bl@bl2)) ty') in
 	    let iscast = d <> None in
             let bindings,ppred =
-	      pr_lconstr_env_n (Global.env()) n iscast
-		(abstract_rawconstr (abstract_rawconstr body bl2) bl) in
+	      pr_lconstr_env_n (Global.env()) iscast (bl@bl2) body in
             (pr_binders_arg bindings,ty,Some (pr_reduce red ++ ppred))
         | ProveBody (bl,t) ->
             (pr_and_type_binders_arg bl, str" :" ++ pr_spc_type t, None)
@@ -720,7 +703,7 @@ let rec pr_vernac = function
       let pr_constructor (coe,(id,c)) =
         hov 2 (pr_lident id ++ str" " ++
                (if coe then str":>" else str":") ++
-                pr_sep_com spc (pr_type_env_n ind_env_params 0) c) in
+                pr_sep_com spc (pr_type_env_n ind_env_params []) c) in
       let pr_constructor_list l = match l with
         | [] -> mt()
         | _ ->
@@ -754,8 +737,10 @@ let rec pr_vernac = function
       let notations = 
 	List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) recs [] in
       let impl = List.map
-        (fun ((recname,_, _, arityc,_),_) -> 
-          let arity = Constrintern.interp_type sigma env0 arityc in
+        (fun ((recname,_, bl, arityc,_),_) -> 
+          let arity =
+            Constrintern.interp_type sigma env0
+              (prod_constr_expr arityc bl) in
 	  let impl_in =
 	    if Impargs.is_implicit_args()
 	    then Impargs.compute_implicits false env0 arity
@@ -776,8 +761,10 @@ let rec pr_vernac = function
 
       let rec_sign = 
         List.fold_left 
-          (fun env ((recname,_,_,arityc,_),_) -> 
-            let arity = Constrintern.interp_type sigma env0 arityc in
+          (fun env ((recname,_,bl,arityc,_),_) -> 
+            let arity =
+              Constrintern.interp_type sigma env0
+                (prod_constr_expr arityc bl) in
             Environ.push_named (recname,None,arity) env)
           (Global.env()) recs in
       
@@ -785,21 +772,19 @@ let rec pr_vernac = 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 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
+        | (id,n,bl,type_,def),ntn ->
             let ids = List.flatten (List.map name_of_binder bl) in
+            let name =
+              try snd (List.nth ids n)
+              with Failure _ ->
+                warn (str "non-printable fixpoint \""++pr_id id++str"\"");
+                Anonymous in
             let annot =
               if List.length ids > 1 then 
-                spc() ++ str "{struct " ++
-                pr_name (snd (List.nth ids n)) ++ str"}"
+                spc() ++ str "{struct " ++ pr_name name ++ str"}"
               else mt() in
-	    let bl, ppc = 
-              pr_lconstr_env_n rec_sign (local_binders_length bl)
-		true (abstract_rawconstr (CCast (dummy_loc,def,type_)) bl) in
+	    let bl,ppc =
+              pr_lconstr_env_n rec_sign true bl (CCast(dummy_loc,def,type_)) in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_type c) type_
             ++ str" :=" ++ brk(1,1) ++ ppc ++ 
@@ -809,8 +794,7 @@ let rec pr_vernac = function
         prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs)
 
   | VernacCoFixpoint corecs ->
-      let pr_onecorec (id,c,def) =
-        let (bl,def,c) = extract_def_binders def c in
+      let pr_onecorec (id,bl,c,def) =
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
         spc() ++ pr_type c ++
         str" :=" ++ brk(1,1) ++ pr_lconstr def in