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

1 files changed, 4 insertions, 6 deletions

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 ] ]