diff options
| author | filliatr | 1999-10-08 08:24:45 +0000 |
|---|---|---|
| committer | filliatr | 1999-10-08 08:24:45 +0000 |
| commit | 05c710f373ed0936d3c67b3189e5db13d2b9ab70 (patch) | |
| tree | 3e2e9fcbfd3c23d93ee21bce0d75be4ac589b3c4 /library | |
| parent | fd28f10096f82ef133bbf10512c8bee617b6b8b3 (diff) | |
deplacement des var. ex. dans proofs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@94 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 3 | ||||
| -rw-r--r-- | library/global.mli | 6 |
2 files changed, 1 insertions, 8 deletions
diff --git a/library/global.ml b/library/global.ml index f7fac03139..6385e932f4 100644 --- a/library/global.ml +++ b/library/global.ml @@ -19,9 +19,7 @@ let _ = (* Then we export the functions of [Typing] on that environment. *) -let evar_map () = evar_map !global_env let universes () = universes !global_env -let metamap () = metamap !global_env let context () = context !global_env let push_var idc = global_env := push_var idc !global_env @@ -36,7 +34,6 @@ let lookup_rel n = lookup_rel n !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_meta n = lookup_meta n !global_env let export s = export !global_env s let import cenv = global_env := import cenv !global_env diff --git a/library/global.mli b/library/global.mli index e959c60914..89cc83cbd5 100644 --- a/library/global.mli +++ b/library/global.mli @@ -6,7 +6,6 @@ open Names open Univ open Term open Sign -open Evd open Constant open Inductive open Environ @@ -17,11 +16,9 @@ open Typing The functions below are the exactly the same as the ones in [Typing], operating on that global environment. *) -val env : unit -> unit environment +val env : unit -> environment -val evar_map : unit -> unit evar_map val universes : unit -> universes -val metamap : unit -> (int * constr) list val context : unit -> context val push_var : identifier * constr -> unit @@ -36,7 +33,6 @@ val lookup_rel : int -> name * typed_type val lookup_constant : section_path -> constant_body val lookup_mind : section_path -> mutual_inductive_body val lookup_mind_specif : constr -> mind_specif -val lookup_meta : int -> constr val export : string -> compiled_env val import : compiled_env -> unit |