mach et himsg; typage sans extraction

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

1 files changed, 12 insertions, 1 deletions

diff --git a/kernel/environ.mli b/kernel/environ.mli
index ec148edaa..60006e82f 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -7,30 +7,35 @@ open Constant
 open Inductive
 open Evd
 open Univ
+open Sign
 
 type 'a unsafe_env
 
 val evar_map : 'a unsafe_env -> 'a evar_map
 val universes : 'a unsafe_env -> universes
 val metamap : 'a unsafe_env -> (int * constr) list
+val context : 'a unsafe_env -> environment
 
 val push_var : identifier * typed_type -> 'a unsafe_env -> 'a unsafe_env
 val push_rel : name * typed_type -> 'a unsafe_env -> 'a unsafe_env
 val set_universes : universes -> 'a unsafe_env -> 'a unsafe_env
 
 val add_constant : constant_entry -> 'a unsafe_env -> 'a unsafe_env
-val add_mind : mind_entry -> 'a unsafe_env -> 'a unsafe_env
+val add_mind : mutual_inductive_entry -> 'a unsafe_env -> 'a unsafe_env
 
 val new_meta : unit -> int
 
 val lookup_var : identifier -> 'a unsafe_env -> name * typed_type
 val lookup_rel : int -> 'a unsafe_env -> name * typed_type
 val lookup_constant : section_path -> 'a unsafe_env -> constant_entry
+val lookup_mind : section_path -> 'a unsafe_env -> mutual_inductive_entry
+val lookup_mind_specif : constr -> 'a unsafe_env -> mind_specif
 val lookup_meta : int -> 'a unsafe_env -> constr
 
 val id_of_global : 'a unsafe_env -> sorts oper -> identifier
 val id_of_name_using_hdchar : 'a unsafe_env -> constr -> name -> identifier
 val named_hd : 'a unsafe_env -> constr -> name -> name
+val prod_name : name * constr * constr -> constr
 
 val translucent_abst : 'a unsafe_env -> constr -> bool
 val evaluable_abst : 'a unsafe_env -> constr -> bool
@@ -51,3 +56,9 @@ val mind_of_path : section_path -> mutual_inductive_entry
 val mind_path : constr -> section_path
 val mind_nparams : 'a unsafe_env -> constr -> int
 val mindsp_nparams : 'a unsafe_env -> section_path -> int
+
+type unsafe_judgment = { 
+  uj_val : constr;
+  uj_type : constr;
+  uj_kind : constr }
+