Suite restructuration inductifs; changement nom module Constant en Declarations

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

1 files changed, 6 insertions, 11 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 93426fde9b..9c56db03a5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@ open Util
 open Options
 open Generic
 open Term
-open Constant
+open Declarations
 open Inductive
 open Reduction
 open Tacred
@@ -359,17 +359,12 @@ let build_scheme lnamedepindsort =
                 (inductive_of_ident indid,dep,s)) lnamedepindsort
   in
   let n = NeverDischarge in 
-  let listdecl = Indrec.build_indrec env0 sigma lrecspec in 
-  let rec declare i = function 
-    | fi::lf -> 
-	let ce = 
-	  { const_entry_body = Cooked listdecl.(i); const_entry_type = None } 
-	in
-	declare_constant fi (ce,n);
-        declare (i+1) lf
-    | _        -> ()
+  let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in 
+  let rec declare decl fi =
+    let ce = { const_entry_body = Cooked decl; const_entry_type = None } 
+    in declare_constant fi (ce,n)
   in 
-  declare 0 lrecnames; 
+  List.iter2 declare listdecl lrecnames; 
   if is_verbose() then pPNL(recursive_message lrecnames)
 
 let start_proof_com s stre com =