Réorganisation suite ajout de constantes locales dans les Records

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

4 files changed, 44 insertions, 20 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 123cbd188f..3fd30327e7 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -427,9 +427,28 @@ let elimination_suffix = function
   | Prop Null -> "_ind"
   | Prop Pos  -> "_rec"
 
+let declare_one_elimination mispec =
+  let mindstr = string_of_id (mis_typename mispec) in
+  let declare na c =
+    declare_constant (id_of_string na)
+      (ConstantEntry { const_entry_body = c; const_entry_type = None }, 
+       NeverDischarge,false);
+    if Options.is_verbose() then pPNL [< 'sTR na; 'sTR " is defined" >]
+  in
+  let env = Global.env () in
+  let sigma = Evd.empty in
+  let elim_scheme = build_indrec env sigma mispec in
+  let npars = mis_nparams mispec in
+  let make_elim s = instanciate_indrec_scheme s npars elim_scheme in
+  let kelim = mis_kelim mispec in
+  List.iter
+    (fun (sort,suff) -> 
+       if List.mem sort kelim then declare (mindstr^suff) (make_elim sort))
+    eliminations
+(*
 let declare_eliminations sp i =
   let mib = Global.lookup_mind sp in
-  let ids = ids_of_named_context mib.mind_hyps in
+
   if not (list_subset ids (ids_of_named_context (Global.named_context ()))) then
     error ("Declarations of elimination scheme outside the section "^
     "of the inductive definition is not implemented");
@@ -452,6 +471,18 @@ let declare_eliminations sp i =
     (fun (sort,suff) -> 
        if List.mem sort kelim then declare (mindstr^suff) (make_elim sort))
     eliminations
+*)
+let declare_eliminations sp =
+  let mib = Global.lookup_mind sp in
+  let ids = ids_of_named_context mib.mind_hyps in
+  if not (list_subset ids (ids_of_named_context (Global.named_context ()))) then    error ("Declarations of elimination scheme outside the section "^
+    "of the inductive definition is not implemented");
+  let ctxt = instance_from_named_context mib.mind_hyps in
+  for i = 0 to Array.length mib.mind_packets - 1 do
+    if mind_type_finite mib i then
+      let mispec = Global.lookup_mind_specif ((sp,i), Array.of_list ctxt) in 
+      declare_one_elimination mispec
+  done
 
 (* Look up function for the default elimination constant *)
 
diff --git a/library/declare.mli b/library/declare.mli
index b902be207b..927f05fde1 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -45,7 +45,9 @@ val declare_parameter : identifier -> constr -> unit
 
 val declare_mind : mutual_inductive_entry -> section_path
 
-val declare_eliminations : section_path -> int -> unit
+(* [declare_eliminations sp] declares elimination schemes associated
+   to the mutual inductive block refered by [sp] *)
+val declare_eliminations : section_path -> unit
 
 val out_inductive : Libobject.obj -> mutual_inductive_entry 
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 2055e5b8af..c4119ccbfb 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -148,8 +148,7 @@ let interp_mutual lparams lnamearconstrs finite =
       (fun acc (id,_,l) -> id::(List.map fst l)@acc) [] lnamearconstrs in
   if not (list_distinct allnames) then
     error "Two inductive objects have the same name";
-  let lrecnames = List.map (fun (x,_,_) -> x)  lnamearconstrs
-  and nparams = List.length lparams
+  let nparams = List.length lparams
   and sigma = Evd.empty 
   and env0 = Global.env() in
   let env_params, params =
@@ -190,24 +189,19 @@ let interp_mutual lparams lnamearconstrs finite =
 	   mind_entry_lc = constrs })
       (List.rev arityl) lnamearconstrs
   in
-  { mind_entry_finite = finite; mind_entry_inds = mispecvec },
-  lrecnames
+  { mind_entry_finite = finite; mind_entry_inds = mispecvec }
 
-let declare_mutual_with_eliminations mie lrecnames finite =
+let declare_mutual_with_eliminations mie =
+  let lrecnames =
+    List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
   let sp = declare_mind mie in
   if is_verbose() then pPNL(minductive_message lrecnames);
-  if finite then
-    for i = 0 to List.length lrecnames - 1 do
-      declare_eliminations sp i
-    done;
+  declare_eliminations sp;
   sp
 
-let build_mutual_give_path lparams lnamearconstrs finite =
-  let mie, lrecnames = interp_mutual lparams lnamearconstrs finite in
-  declare_mutual_with_eliminations mie lrecnames finite
-
 let build_mutual lparams lnamearconstrs finite =
-  let _ = build_mutual_give_path lparams lnamearconstrs finite in ()
+  let mie = interp_mutual lparams lnamearconstrs finite in
+  let _ = declare_mutual_with_eliminations mie in ()
 
 (* try to find non recursive definitions *)
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 44bf292667..c0479acf6c 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -30,10 +30,7 @@ val build_mutual :
   (identifier * Coqast.t) list -> 
     (identifier * Coqast.t * (identifier * Coqast.t) list) list -> bool -> unit
 
-val build_mutual_give_path : 
-  (identifier * Coqast.t) list -> 
-    (identifier * Coqast.t * (identifier * Coqast.t) list) list -> bool
-      -> section_path
+val declare_mutual_with_eliminations : Declarations.mutual_inductive_entry -> section_path
 
 val build_recursive :
   (identifier * ((identifier * Coqast.t) list) * Coqast.t * Coqast.t) list