GROS COMMIT:

 - reduction du noyau (variables existentielles, fonctions auxiliaires
   pour inventer des noms, etc. deplacees hors de kernel/)
 - changement de noms de constructeurs des constr (suppression de "Is" et
   "Mut")


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

1 files changed, 22 insertions, 54 deletions

diff --git a/library/global.ml b/library/global.ml
index b55f741dd..3f009d6d2 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -11,7 +11,6 @@
 open Util
 open Names
 open Term
-open Instantiate
 open Sign
 open Environ
 open Safe_typing
@@ -35,69 +34,38 @@ let _ =
 
 (* Then we export the functions of [Typing] on that environment. *)
 
-let universes () = universes !global_env
-let context () = context !global_env
-let named_context () = named_context !global_env
-
-let push_named_def idc =
-  let d, env = check_and_push_named_def idc !global_env in
-  global_env := env; d
-
-let push_named_assum idc =
-  let d, env = check_and_push_named_assum idc !global_env in
-  global_env := env; d
+let universes () = universes (env())
+let named_context () = named_context (env())
+
+let push_named_assum a =
+  let (cst,env) = push_named_assum a !global_env in
+  global_env := env;
+  cst
+let push_named_def d =
+  let (cst,env) = push_named_def d !global_env in
+  global_env := env;
+  cst
+let pop_named_decls ids = global_env := pop_named_decls ids !global_env
 
-let add_parameter sp c l = global_env := add_parameter sp c l !global_env
-let add_constant sp ce l = global_env := add_constant sp ce l !global_env
-let add_discharged_constant sp r l = 
-  global_env := add_discharged_constant sp r l !global_env
-let add_mind sp mie l = global_env := add_mind sp mie l !global_env
+let add_parameter sp c = global_env := add_parameter sp c !global_env
+let add_constant sp ce = global_env := add_constant sp ce !global_env
+let add_discharged_constant sp r = 
+  global_env := add_discharged_constant sp r !global_env
+let add_mind sp mie = global_env := add_mind sp mie !global_env
 let add_constraints c = global_env := add_constraints c !global_env
 
-let pop_named_decls ids = global_env := pop_named_decls ids !global_env
-
-let lookup_named id = lookup_named id !global_env
-let lookup_constant sp = lookup_constant sp !global_env
-let lookup_mind sp = lookup_mind sp !global_env
-let lookup_mind_specif c = lookup_mind_specif c !global_env
+let lookup_named id = lookup_named id (env())
+let lookup_constant sp = lookup_constant sp (env())
+let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind
+let lookup_mind sp = lookup_mind sp (env())
 
 let export s = export !global_env s
 let import cenv = global_env := import cenv !global_env
 
-(* Some instanciations of functions from [Environ]. *)
-
-let sp_of_global ref = Environ.sp_of_global (env_of_safe_env !global_env) ref
-
-(* To know how qualified a name should be to be understood in the current env*)
-
-let qualid_of_global ref =  
-  let sp = sp_of_global ref in
-  let id = basename sp in
-  let rec find_visible dir qdir =
-    let qid = Nametab.make_qualid qdir id in
-    if (try Nametab.locate qid = ref with Not_found -> false) then qid
-    else match dir with
-      | [] -> Nametab.qualid_of_sp sp
-      | a::l -> find_visible l (add_dirpath_prefix a qdir)
-  in
-  find_visible (rev_repr_dirpath (dirpath sp)) (make_dirpath [])
-
-let string_of_global ref = Nametab.string_of_qualid (qualid_of_global ref)
-
 (*s Function to get an environment from the constants part of the global
     environment and a given context. *)
 
 let env_of_context hyps = 
-  change_hyps (fun _ -> hyps) (env_of_safe_env !global_env)
-
-(* Functions of [Inductive], composed with [lookup_mind_specif]. *)
-(* Rem:Cannot open Inductive to avoid clash with Inductive.lookup_mind_specif*)
-
-let mind_is_recursive =
-  Util.compose Inductive.mis_is_recursive lookup_mind_specif 
-
-let mind_nconstr = Util.compose Inductive.mis_nconstr lookup_mind_specif
-let mind_nparams = Util.compose Inductive.mis_nparams lookup_mind_specif
-let mind_nf_lc = Util.compose Inductive.mis_nf_lc lookup_mind_specif
+  reset_with_named_context hyps (env())