Keep structure information for Fixpoint declaration and Fix terms

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

6 files changed, 9 insertions, 7 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 533919b676..8e3820c3a5 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -237,7 +237,7 @@ 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,t,d) -> (id,n,subst t,subst d)) dl)
+      CFix (loc,id,List.map (fun (id,n,on, t,d) -> (id,n, on,subst t,subst d)) dl)
   | CCoFix (_,id,dl) ->
       CCoFix (loc,id,List.map (fun (id,t,d) -> (id,subst t,subst d)) dl)
   in subst a
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 4e0d1118f3..3e513f0719 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -339,14 +339,14 @@ GEXTEND Gram
   fixbinder:
     [ [ id = base_ident; "/"; recarg = natural; ":"; type_ = constr;
         ":="; def = constr ->
-          (id, recarg-1, type_, def)
+          (id, recarg-1, None, 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, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)) ] ]
+	  (id, ni, None, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)) ] ]
   ;
   fixbinders:
     [ [ fbs = LIST1 fixbinder SEP "with" -> fbs ] ]
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 101c29d31f..fb770768a9 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -84,10 +84,11 @@ let rec index_of_annot bl ann =
 
 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 ty = match tyc with
       None -> CHole tloc
     | Some t -> mkCProdN loc bl t in
-  (snd id,n,ty,mkCLambdaN loc bl body)
+  (snd id,n,Some nargs,ty,mkCLambdaN loc bl body)
 
 let mk_cofixb (loc,id,bl,ann,body,(tloc,tyc)) =
   let _ = option_app (fun (aloc,_) ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ad3862388e..def4b9fbf9 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -255,7 +255,7 @@ GEXTEND Gram
           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, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)), ntn) ] ]
+	  ((id, ni, None, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)), ntn) ] ]
   ;
   specifrec:
     [ [ l = LIST1 onerec SEP "with" -> l ] ]
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index c7fdcdc576..fd4647a620 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -205,6 +205,7 @@ GEXTEND Gram
         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 ni =
             match annot with
                 Some id ->
@@ -221,7 +222,7 @@ GEXTEND Gram
           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, G_constrnew.mkCProdN loc1 bl type_,
+	  ((id, ni, Some nargs, G_constrnew.mkCProdN loc1 bl type_,
 	    G_constrnew.mkCLambdaN loc2 bl def),ntn) ] ]
   ;
   corec_definition:
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index cdc7cc6f76..77853c5e1a 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -155,7 +155,7 @@ 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 pr_fixdecl pr (id,n,_,t,c) =
   let (bl,t,c) = split_fix (n+1) t c in
   pr_recursive_decl pr id 
     (brk (1,2) ++ str "[" ++ pr_binders pr bl ++ str "]") t c