mach -> typing; machops -> typeops

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

1 files changed, 58 insertions, 0 deletions

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
new file mode 100644
index 000000000..1a3b729c2
--- /dev/null
+++ b/kernel/typeops.mli
@@ -0,0 +1,58 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Univ
+open Term
+open Environ
+(*i*)
+
+
+(* Base operations of the typing machine. *)
+
+val make_judge : constr -> typed_type -> unsafe_judgment
+
+val j_val_only : unsafe_judgment -> constr
+
+val typed_type_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type
+
+val relative : 'a unsafe_env -> int -> unsafe_judgment
+
+val type_of_constant_or_existential : 'a unsafe_env -> constr -> typed_type
+
+val type_of_inductive : 'a unsafe_env -> constr -> typed_type
+
+val type_of_constructor : 'a unsafe_env -> constr -> constr
+
+val type_of_case : 'a unsafe_env -> unsafe_judgment -> unsafe_judgment 
+  -> unsafe_judgment array -> unsafe_judgment
+
+val type_of_prop_or_set : contents -> unsafe_judgment
+
+val type_of_type : universe -> universes -> unsafe_judgment * universes
+
+val assumption_of_judgement : 'a unsafe_env -> unsafe_judgment -> typed_type
+
+val abs_rel : 
+  'a unsafe_env -> name -> typed_type -> unsafe_judgment 
+    -> unsafe_judgment * universes
+
+val gen_rel :
+  'a unsafe_env -> name -> typed_type -> unsafe_judgment 
+    -> unsafe_judgment * universes
+
+val cast_rel : 
+  'a unsafe_env -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment
+
+val apply_rel_list : 
+  'a unsafe_env -> bool -> unsafe_judgment list -> unsafe_judgment
+    -> unsafe_judgment * universes
+
+val check_fix : 'a unsafe_env -> constr -> unit
+val check_cofix : 'a unsafe_env -> constr -> unit
+
+val type_fixpoint : 'a unsafe_env -> name list -> typed_type array 
+    -> unsafe_judgment array -> universes
+
+