- 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, 22 insertions, 22 deletions

diff --git a/kernel/sign.mli b/kernel/sign.mli
index 2a0a567dec..e2ef7d4a1e 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -54,35 +54,35 @@ val dbindv : 'a signature -> 'b term array -> 'a * 'b term
 (*s Signatures with named and de Bruijn variables. *)
 
 type 'a db_signature = (name * 'a) list
-type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature
-
-val gLOB : 'b signature -> ('b,'a) env
-
-val add_rel : (name * 'a) -> ('b,'a) env -> ('b,'a) env 
-val add_glob : (identifier * 'b) -> ('b,'a) env -> ('b,'a) env
-val lookup_glob : identifier -> ('b,'a) env -> (identifier * 'b)
-val lookup_rel : int -> ('b,'a) env  -> (name * 'a)
-val mem_glob : identifier -> ('b,'a) env -> bool
-
-val get_globals : ('b,'a) env -> 'b signature
-val get_rels : ('b,'a) env -> 'a db_signature
-val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) env -> 'c -> 'c
-val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) env -> 'c
-val map_rel_env : ('a -> 'b) -> ('c,'a) env -> ('c,'b) env
-val map_var_env : ('c -> 'b) -> ('c,'a) env -> ('b,'a) env
-val isnull_rel_env : ('a,'b) env -> bool
-val uncons_rel_env : ('a,'b) env -> (name * 'b) * ('a,'b) env
-val ids_of_env : ('a, 'b) env -> identifier list
+type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature
+
+val gLOB : 'b signature -> ('b,'a) sign
+
+val add_rel : (name * 'a) -> ('b,'a) sign -> ('b,'a) sign 
+val add_glob : (identifier * 'b) -> ('b,'a) sign -> ('b,'a) sign
+val lookup_glob : identifier -> ('b,'a) sign -> (identifier * 'b)
+val lookup_rel : int -> ('b,'a) sign  -> (name * 'a)
+val mem_glob : identifier -> ('b,'a) sign -> bool
+
+val get_globals : ('b,'a) sign -> 'b signature
+val get_rels : ('b,'a) sign -> 'a db_signature
+val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) sign -> 'c -> 'c
+val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) sign -> 'c
+val map_rel_env : ('a -> 'b) -> ('c,'a) sign -> ('c,'b) sign
+val map_var_env : ('c -> 'b) -> ('c,'a) sign -> ('b,'a) sign
+val isnull_rel_env : ('a,'b) sign -> bool
+val uncons_rel_env : ('a,'b) sign -> (name * 'b) * ('a,'b) sign
+val ids_of_env : ('a, 'b) sign -> identifier list
 
 type ('b,'a) search_result =
   | GLOBNAME of identifier  * 'b
   | RELNAME of int * 'a
 
-val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result
+val lookup_id : identifier -> ('b,'a) sign -> ('b,'a) search_result
 
 
-type 'b assumptions = (typed_type,'b) env
-type context = (typed_type,typed_type) env
+type 'b assumptions = (typed_type,'b) sign
+type context = (typed_type,typed_type) sign
 type var_context = typed_type signature
 
 val unitize_env : 'a assumptions -> unit assumptions