Ajout possibilité clause "where" dans co-points fixes

(+ uniformisation position notation dans les blocs inductifs et récursifs)


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

7 files changed, 33 insertions, 32 deletions

diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index a24e5845b5..5f09b3590a 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1194,11 +1194,10 @@ let do_build_inductive
       (rel_constructors)
   in
   let rel_ind i ext_rel_constructors = 
-    (dummy_loc,relnames.(i)),
-    None,
+    ((dummy_loc,relnames.(i)),
     rel_params,
     rel_arities.(i),
-    ext_rel_constructors
+    ext_rel_constructors),None
   in
   let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in 
   let rel_inds = Array.to_list ext_rel_constructors in 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index b231a48bfd..88a9014eec 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1890,7 +1890,7 @@ let rec xlate_vernac =
          build_record_field_list field_list)
    | VernacInductive (isind, lmi) ->
       let co_or_ind = if isind then "Inductive" else "CoInductive" in
-      let strip_mutind ((_,s), notopt, parameters, c, constructors) =
+      let strip_mutind (((_,s), parameters, c, constructors), notopt) =
           CT_ind_spec
             (xlate_ident s, xlate_binder_list parameters, xlate_formula c,
              build_constructors constructors,
@@ -1899,7 +1899,7 @@ 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),boxed) ->
-      let strip_mutrec ((fid, (n, ro), bl, arf, ardef), ntn) =
+      let strip_mutrec ((fid, (n, ro), bl, arf, ardef), _ntn) =
         let (struct_arg,bl,arf,ardef) =
 	 (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
 	 (* By the way, how could [bl = []] happen in V8 syntax ?  *)
@@ -1919,7 +1919,7 @@ let rec xlate_vernac =
 	  (CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))
    | VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive"
    | VernacCoFixpoint ((lm :: lmi),boxed) ->
-      let strip_mutcorec (fid, bl, arf, ardef) =
+      let strip_mutcorec ((fid, bl, arf, ardef), _ntn) =
 	CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
                       xlate_formula arf, xlate_formula ardef) in
         CT_cofix_decl
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 737c97bae3..510fe529f0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -191,9 +191,9 @@ GEXTEND Gram
     ;
   (* Inductives and records *)
   inductive_definition:
-    [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr; 
+    [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr;
         ":="; lc = constructor_list; ntn = decl_notation ->
-	  (id,ntn,indpar,c,lc) ] ]
+	  ((id,indpar,c,lc),ntn) ] ]
   ;
   constructor_list:
     [ [ "|"; l = LIST1 constructor SEP "|" -> l
@@ -212,7 +212,7 @@ GEXTEND Gram
   (* (co)-fixpoints *)
   rec_definition:
     [ [ id = ident; bl = LIST1 binder_let;
-        annot = rec_annotation; type_ = type_cstr; 
+        annot = rec_annotation; ty = type_cstr; 
 	":="; def = lconstr; ntn = decl_notation ->
           let names = List.map snd (names_of_local_assums bl) in
           let ni =
@@ -227,12 +227,12 @@ GEXTEND Gram
 		     otherwise, we search the recursive index later *)
 		  if List.length names = 1 then Some 0 else None	  
 	  in 
-	  ((id, (ni, snd annot), bl, type_, def),ntn) ] ]
+	  ((id,(ni,snd annot),bl,ty,def),ntn) ] ]
   ;
   corec_definition:
-    [ [ id = ident; bl = LIST0 binder_let; c = type_cstr; ":=";
-        def = lconstr ->
-          (id,bl,c ,def) ] ]
+    [ [ id = ident; bl = LIST0 binder_let; ty = type_cstr; ":=";
+        def = lconstr; ntn = decl_notation ->
+          ((id,bl,ty,def),ntn) ] ]
   ;
   rec_annotation:
     [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index b3a8abce55..5e13a11245 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -530,7 +530,7 @@ let rec pr_vernac = function
             fnl() ++
             str (if List.length l = 1 then "   " else " | ") ++
             prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l in
-      let pr_oneind key (id,ntn,indpar,s,lc) =
+      let pr_oneind key ((id,indpar,s,lc),ntn) =
 	hov 0 (
           str key ++ spc() ++
           pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ 
@@ -585,14 +585,16 @@ let rec pr_vernac = function
         prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs)
 
   | VernacCoFixpoint (corecs,b) ->
-      let pr_onecorec (id,bl,c,def) =
+      let pr_onecorec ((id,bl,c,def),ntn) =
         let (bl',def,c) =
               if Options.do_translate() then extract_def_binders def c
               else ([],def,c) in
         let bl = bl @ bl' in
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
         spc() ++ pr_lconstr_expr c ++
-        str" :=" ++ brk(1,1) ++ pr_lconstr def in
+        str" :=" ++ brk(1,1) ++ pr_lconstr def  ++ 
+	pr_decl_notation pr_constr ntn
+      in
       let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in
       hov 1 (str start ++ spc() ++
       prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs)  
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 720df5a80c..24d292d49f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -381,10 +381,10 @@ let eq_local_binders bl1 bl2 =
 let extract_coercions indl =
   let mkqid (_,((_,id),_)) = make_short_qualid id in
   let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in
-  List.map mkqid (List.flatten(List.map (fun (_,_,_,_,lc) -> extract lc) indl))
+  List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl))
 
 let extract_params indl =
-  let paramsl = List.map (fun (_,_,params,_,_) -> params) indl in
+  let paramsl = List.map (fun (_,params,_,_) -> params) indl in
   match paramsl with
   | [] -> anomaly "empty list of inductive types"
   | params::paramsl ->
@@ -392,13 +392,13 @@ let extract_params indl =
 	"Parameters should be syntactically the same for each inductive type";
       params
 
-let prepare_inductive indl =
-  let ntnl,indl =
-    List.split (List.map (fun ((_,indname),ntn,_,ar,lc) -> ntn, { 
+let prepare_inductive ntnl indl =
+  let indl =
+    List.map (fun ((_,indname),_,ar,lc) -> { 
       ind_name = indname;
       ind_arity = ar;
       ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
-    }) indl) in
+    }) indl in
   List.fold_right option_cons ntnl [], indl
 
 let declare_mutual_with_eliminations isrecord mie =
@@ -408,10 +408,11 @@ let declare_mutual_with_eliminations isrecord mie =
   declare_eliminations kn;
   kn
 
-let build_mutual indl finite =
+let build_mutual l finite =
+  let indl,ntnl = List.split l in
   let paramsl = extract_params indl in
   let coes = extract_coercions indl in
-  let notations,indl = prepare_inductive indl in
+  let notations,indl = prepare_inductive ntnl indl in
   let mie = interp_mutual paramsl indl notations finite in
   (* Declare the mutual inductive block with its eliminations *)
   ignore (declare_mutual_with_eliminations false mie);
@@ -604,8 +605,8 @@ let build_recursive l b =
   interp_recursive (IsFixpoint g) fixl b
 
 let build_corecursive l b =
-  let fixl = List.map (fun (id,bl,typ,def) -> 
-    ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},None))
+  let fixl = List.map (fun ((id,bl,typ,def),ntn) -> 
+    ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn))
     l in
   interp_recursive IsCoFixpoint fixl b
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index be589da1a3..7c3d519469 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -39,14 +39,14 @@ val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit
 val declare_assumption : identifier located list ->
   coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> unit
 
-val build_mutual : inductive_expr list -> bool -> unit
+val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit
 
 val declare_mutual_with_eliminations :
   bool -> Entries.mutual_inductive_entry -> mutual_inductive
 
 val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit
 
-val build_corecursive : cofixpoint_expr list -> bool -> unit
+val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit
 
 val build_scheme : (identifier located * bool * reference * rawsort) list -> unit
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 51010afa80..8b654e12d2 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -146,8 +146,7 @@ type simple_binder = lident list  * constr_expr
 type 'a with_coercion = coercion_flag * 'a
 type constructor_expr = (lident * constr_expr) with_coercion
 type inductive_expr =
-     lident * decl_notation * local_binder list * constr_expr
-    * constructor_expr list
+     lident * local_binder list * constr_expr * constructor_expr list
 type definition_expr =
   | ProveBody of local_binder list * constr_expr
   | DefineBody of local_binder list * raw_red_expr option * constr_expr
@@ -195,9 +194,9 @@ type vernac_expr =
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * simple_binder with_coercion list
-  | VernacInductive of inductive_flag * inductive_expr list
+  | VernacInductive of inductive_flag * (inductive_expr * decl_notation) list
   | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool
-  | VernacCoFixpoint of cofixpoint_expr list * bool
+  | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool
   | VernacScheme of (lident * bool * lreference * sort_expr) list
 
   (* Gallina extensions *)