- Typing -> Safe_typing

 - proofs/Typing_ev -> pretyping/Typing
 - env -> sign
 - fonctions var_context


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

1 files changed, 0 insertions, 77 deletions

diff --git a/kernel/typing.mli b/kernel/typing.mli
deleted file mode 100644
index 10530d123b..0000000000
--- a/kernel/typing.mli
+++ /dev/null
@@ -1,77 +0,0 @@
-
-(* $Id$ *)
-
-(*i*)
-open Pp
-open Names
-open Term
-open Univ
-open Sign
-open Constant
-open Inductive
-open Environ
-open Typeops
-(*i*)
-
-(*s Safe environments. Since we are now able to type terms, we can define an
-  abstract type of safe environments, where objects are typed before being
-  added. Internally, the datatype is still [unsafe_env]. We re-export the
-  functions of [Environ] for the new type [environment]. *)
-
-type environment
-
-val empty_environment : environment
-
-val universes : environment -> universes
-val context : environment -> context
-
-val push_var : identifier * constr -> environment -> environment
-val push_rel : name * constr -> environment -> environment
-val add_constant : 
-  section_path -> constant_entry -> environment -> environment
-val add_parameter :
-  section_path -> constr -> environment -> environment
-val add_mind : 
-  section_path -> mutual_inductive_entry -> environment -> environment
-val add_constraints : constraints -> environment -> environment
-
-val lookup_var : identifier -> environment -> name * typed_type
-val lookup_rel : int -> environment -> name * typed_type
-val lookup_constant : section_path -> environment -> constant_body
-val lookup_mind : section_path -> environment -> mutual_inductive_body
-val lookup_mind_specif : constr -> environment -> mind_specif
-
-val export : environment -> string -> compiled_env
-val import : compiled_env -> environment -> environment
-
-val unsafe_env_of_env : environment -> unsafe_env
-
-(*s Typing without information. *)
-
-type judgment
-
-val j_val : judgment -> constr
-val j_type : judgment -> constr
-val j_kind : judgment -> constr
-
-val safe_machine : environment -> constr -> judgment * constraints
-val safe_machine_type : environment -> constr -> typed_type
-
-val fix_machine : environment -> constr -> judgment * constraints
-val fix_machine_type : environment -> constr -> typed_type
-
-val unsafe_machine : environment -> constr -> judgment * constraints
-val unsafe_machine_type : environment -> constr -> typed_type
-
-val type_of : environment -> constr -> constr
-
-val type_of_type : environment -> constr -> constr
-
-val unsafe_type_of : environment -> constr -> constr
-
-
-(*s Typing with information (extraction). *)
-
-type information = Logic | Inf of judgment
-
-