Déplacement de Declare juste à la fin de interp pour pouvoir accéder à interp

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

6 files changed, 70 insertions, 81 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index aa5057db8..03a0da56a 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -17,7 +17,6 @@ open Nametab
 open Environ
 open Libobject
 open Library
-open Declare
 open Term
 open Termops
 open Rawterm
@@ -240,11 +239,6 @@ let inductive_class_of ind = fst (class_info (CL_IND ind))
 
 let class_args_of c = snd (decompose_app c)
 
-let strength_of_cl = function 
-  | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn))
-  | CL_SECVAR sp -> variable_strength sp
-  | _ -> Global
-
 let string_of_class = function
   | CL_FUN -> if !Options.v7 then "FUNCLASS" else "Funclass"
   | CL_SORT -> if !Options.v7 then "SORTCLASS" else "Sortclass"
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index aa0cca3dc..07f1623f8 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -14,7 +14,6 @@ open Decl_kinds
 open Term
 open Evd
 open Environ
-open Declare
 open Nametab
 (*i*)
 
@@ -26,6 +25,8 @@ type cl_typ =
   | CL_CONST of constant
   | CL_IND of inductive
 
+val subst_cl_typ : substitution -> cl_typ -> cl_typ
+
 (* This is the type of infos for declared classes *)
 type cl_info_typ = {
   cl_strength : strength;
@@ -66,8 +67,6 @@ val inductive_class_of : inductive -> cl_index
 
 val class_args_of : constr -> constr list
 
-val strength_of_cl : cl_typ -> strength
-
 (*s [declare_coercion] adds a coercion in the graph of coercion paths *)
 val declare_coercion : 
   coe_typ -> unsafe_judgment -> strength -> isid:bool ->
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index bf7e13158..f9bd67b36 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -25,7 +25,6 @@ open Reductionops
 open Typeops
 open Type_errors
 open Indtypes (* pour les erreurs *)
-open Declare
 open Safe_typing
 open Nametab
 
@@ -405,7 +404,8 @@ let instanciate_indrec_scheme sort =
   in
   drec
 
-(* Change the sort in the type of an inductive definition, builds the corresponding eta-expanded term *)
+(* Change the sort in the type of an inductive definition, builds the
+   corresponding eta-expanded term *)
 let instanciate_type_indrec_scheme sort npars term =
   let rec drec np elim =
     match kind_of_term elim with
@@ -490,66 +490,12 @@ let type_rec_branches recursive env sigma indt p c =
 
 (*s Eliminations. *)
 
-let type_suff = "_rect"
-
-let non_type_eliminations = [ (InProp,"_ind") ; (InSet,"_rec")]
-
 let elimination_suffix = function
   | InProp -> "_ind"
   | InSet  -> "_rec"
   | InType -> "_rect"
 
 let make_elimination_ident id s = add_suffix id (elimination_suffix s)
-  
-let declare_one_elimination ind =
-  let (mib,mip) = Global.lookup_inductive ind in 
-  let mindstr = string_of_id mip.mind_typename in
-  let declare na c t =
-    let kn = Declare.declare_constant (id_of_string na)
-      (DefinitionEntry
-        { const_entry_body = c;
-          const_entry_type = t;
-          const_entry_opaque = false }, 
-       Decl_kinds.IsDefinition) in
-    Options.if_verbose ppnl (str na ++ str " is defined"); 
-    kn
-  in
-  let env = Global.env () in
-  let sigma = Evd.empty in
-  let elim_scheme = build_indrec env sigma ind in
-  let npars = mip.mind_nparams in
-  let make_elim s = instanciate_indrec_scheme s npars elim_scheme in
-  let kelim = mip.mind_kelim in
-(* in case the inductive has a type elimination, generates only one induction scheme, 
-   the other ones share the same code with the apropriate type *)
-   if List.mem InType kelim then
-    let cte =
-      declare (mindstr^type_suff) (make_elim (new_sort_in_family InType)) None
-    in let c = mkConst (snd cte) and t = constant_type (Global.env ()) (snd cte)
-    in List.iter  
-	 (fun (sort,suff) -> 
-            let (t',c') = instanciate_type_indrec_scheme (new_sort_in_family sort) npars c t
-            in let _ = declare (mindstr^suff) c' (Some t')
-            in ())
-	 non_type_eliminations
-   else (* Impredicative or logical inductive definition *)
-     List.iter
-    (fun (sort,suff) -> 
-       if List.mem sort kelim then
-	 let _ = declare (mindstr^suff) (make_elim (new_sort_in_family sort)) None in ())
-     non_type_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");
-*)
-  if mib.mind_finite then
-    for i = 0 to Array.length mib.mind_packets - 1 do
-      declare_one_elimination (sp,i)
-    done
 
 (* Look up function for the default elimination constant *)
 
@@ -563,19 +509,19 @@ let lookup_eliminator ind_sp s =
   let ref = ConstRef (make_kn mp dp (label_of_id id)) in
   try 
     let _ = sp_of_global ref in
-      constr_of_reference ref
+    constr_of_reference ref
   with Not_found ->
   (* Then try to get a user-defined eliminator in some other places *)
   (* using short name (e.g. for "eq_rec") *)
-    try construct_reference None id
-    with Not_found ->
-      errorlabstrm "default_elim"
-	(str "Cannot find the elimination combinator " ++
-           pr_id id ++ spc () ++
-	   str "The elimination of the inductive definition " ++
-           pr_id id ++ spc () ++ str "on sort " ++ 
-           spc () ++ print_sort_family s ++
-	   str " is probably not allowed")
+  try constr_of_reference (Nametab.locate (make_short_qualid id))
+  with Not_found ->
+    errorlabstrm "default_elim"
+      (str "Cannot find the elimination combinator " ++
+       pr_id id ++ spc () ++
+       str "The elimination of the inductive definition " ++
+       pr_id id ++ spc () ++ str "on sort " ++ 
+       spc () ++ print_sort_family s ++
+       str " is probably not allowed")
 
 
 (*  let env = Global.env() in
@@ -588,7 +534,7 @@ let lookup_eliminator ind_sp s =
   with Not_found ->
   (* Then try to get a user-defined eliminator in some other places *)
   (* using short name (e.g. for "eq_rec") *)
-    try construct_reference None id
+    try constr_of_reference (Nametab.locate (make_short_qualid id))
     with Not_found ->
       errorlabstrm "default_elim"
 	(str "Cannot find the elimination combinator " ++
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 38d07d1d9..1ab429dcf 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -30,6 +30,8 @@ val make_case_gen : env -> evar_map -> inductive -> sorts_family -> constr
 
 val build_indrec : env -> evar_map -> inductive -> constr
 val instanciate_indrec_scheme : sorts -> int -> constr -> constr
+val instanciate_type_indrec_scheme : sorts -> int -> constr -> types ->
+  constr * types
 
 (* This builds complex [Scheme] *)
 
@@ -49,7 +51,6 @@ val make_rec_branch_arg :
     constr -> constructor_summary -> wf_paths list -> constr
 
 (* *)
-val declare_eliminations : mutual_inductive -> unit
 val lookup_eliminator : inductive -> sorts_family -> constr
 val elimination_suffix : sorts_family -> string
 val make_elimination_ident : identifier -> sorts_family -> identifier
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 080ed4374..a1d07777b 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -663,6 +663,36 @@ let ids_of_context env =
 let names_of_rel_context env =
   List.map (fun (na,_,_) -> na) (rel_context env)
 
+(**** Globality of identifiers *)
+
+(* TODO temporary hack!!! *)
+let rec is_imported_modpath = function
+  | MPfile dp -> dp <> (Lib.library_dp ())
+(*  | MPdot (mp,_) -> is_imported_modpath mp *)
+  | _ -> false
+
+let is_imported_ref = function
+  | VarRef _ -> false
+  | ConstRef kn 
+  | IndRef (kn,_)
+  | ConstructRef ((kn,_),_) 
+(*  | ModTypeRef ln  *) -> 
+      let (mp,_,_) = repr_kn kn in is_imported_modpath mp
+(*  | ModRef mp ->
+      is_imported_modpath mp
+*)
+
+let is_global id =
+  try 
+    let ref = locate (make_short_qualid id) in
+    not (is_imported_ref ref)
+  with Not_found -> 
+    false
+
+let is_section_variable id =
+  try let _ = Sign.lookup_named id (Global.named_context()) in true
+  with Not_found -> false
+
 (* Nouvelle version de renommage des variables (DEC 98) *)
 (* This is the algorithm to display distinct bound variables 
 
@@ -701,14 +731,11 @@ let occur_id env nenv id0 c =
   with Occur -> true
     | Not_found -> false (* Case when a global is not in the env *)
 
-let is_section_variable id =
-  try let _ = Declare.find_section_variable id in true with Not_found -> false
-
 let next_name_not_occuring env name l env_names t =
   let rec next id =
     if List.mem id l or occur_id env env_names id t or 
       (* To be consistent with intro mechanism *)
-      (Declare.is_global id & not (is_section_variable id))
+      (is_global id & not (is_section_variable id))
     then next (lift_ident id)
     else id
   in 
@@ -826,3 +853,16 @@ let rec rename_bound_var env l c =
         mkProd (Anonymous, c1, rename_bound_var env' l c2)
   | Cast (c,t) -> mkCast (rename_bound_var env l c, t)
   | x -> c
+
+(* References to constr *)
+
+let global_reference id = 
+  constr_of_reference (Nametab.locate (make_short_qualid id))
+
+let construct_reference ctx id =
+  try
+    mkVar (let _ = Sign.lookup_named id ctx in id)
+  with Not_found ->
+    global_reference id
+
+
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 216a090c4..9c9243c8c 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -175,3 +175,12 @@ val make_all_name_different : env -> env
 
 val global_vars : env -> constr -> identifier list
 val global_vars_set_of_decl : env -> named_declaration -> Idset.t
+
+(* References to constr *)
+
+val construct_reference : named_context -> identifier -> constr
+val global_reference : identifier -> constr
+
+(* Test if an identifier is the basename of a global reference *)
+val is_global : identifier -> bool
+