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

3 files changed, 16 insertions, 16 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 720df5a80..24d292d49 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 be589da1a..7c3d51946 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 51010afa8..8b654e12d 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 *)