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, 48 insertions, 0 deletions

diff --git a/kernel/typing.mli b/kernel/typing.mli
new file mode 100644
index 0000000000..9e37c4c798
--- /dev/null
+++ b/kernel/typing.mli
@@ -0,0 +1,48 @@
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+open Names
+open Term
+open Univ
+open Environ
+open Machops
+(*i*)
+
+(*s Machines without information. *)
+
+val safe_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes
+val safe_machine_type : 'a unsafe_env -> constr -> typed_type
+
+val fix_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes
+val fix_machine_type : 'a unsafe_env -> constr -> typed_type
+
+val unsafe_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes
+val unsafe_machine_type : 'a unsafe_env -> constr -> typed_type
+
+val type_of : 'a unsafe_env -> constr -> constr
+
+val type_of_type : 'a unsafe_env -> constr -> constr
+
+val unsafe_type_of : 'a unsafe_env -> constr -> constr
+
+
+(*s Machine with information. *)
+
+type information = Logic | Inf of unsafe_judgment
+
+(*i
+val infexemeta : 
+  'a unsafe_env -> constr -> unsafe_judgment * information * universes
+
+val infexecute_type : 
+  'a unsafe_env -> constr -> typed_type * information * universes
+
+val infexecute : 
+  'a unsafe_env -> constr -> unsafe_judgment * information * universes
+
+val inf_env_of_env : 'a unsafe_env -> 'a unsafe_env
+
+val core_infmachine : 'a unsafe_env -> constr -> information
+i*)