Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 86 insertions, 0 deletions

diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
new file mode 100644
index 00000000..4357e504
--- /dev/null
+++ b/pretyping/pretyping.mli
@@ -0,0 +1,86 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: pretyping.mli,v 1.28.2.1 2004/07/16 19:30:46 herbelin Exp $ i*)
+
+(*i*)
+open Names
+open Sign
+open Term
+open Environ
+open Evd
+open Rawterm
+open Evarutil
+(*i*)
+
+type var_map = (identifier * unsafe_judgment) list
+
+(* constr with holes *)
+type open_constr = evar_map * constr
+
+
+(* Generic call to the interpreter from rawconstr to constr, failing
+   unresolved holes in the rawterm cannot be instantiated.
+
+   In [understand_gen sigma env varmap typopt raw],
+
+   sigma : initial set of existential variables (typically dependent subgoals)
+   varmap : partial subtitution of variables (used for the tactic language)
+   metamap : partial subtitution of meta (used for the tactic language)
+   typopt : is not None, this is the expected type for raw (used to define evars)
+*)
+val understand_gen :
+  evar_map -> env -> var_map
+    -> expected_type:(constr option) -> rawconstr -> constr
+
+val understand_gen_ltac :
+  evar_map -> env -> var_map * (identifier * identifier option) list
+    -> expected_type:(constr option) -> rawconstr -> constr
+
+(* Generic call to the interpreter from rawconstr to constr, turning
+   unresolved holes into metas. Returns also the typing context of
+   these metas. Work as [understand_gen] for the rest. *)
+val understand_gen_tcc :
+  evar_map -> env -> var_map
+    -> constr option -> rawconstr -> open_constr
+
+(* Standard call to get a constr from a rawconstr, resolving implicit args *)
+val understand : evar_map -> env -> rawconstr -> constr
+
+(* Idem but the rawconstr is intended to be a type *)
+val understand_type : evar_map -> env -> rawconstr -> constr
+
+(* Idem but returns the judgment of the understood term *)
+val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
+
+(* Idem but returns the judgment of the understood type *)
+val understand_type_judgment : evar_map -> env -> rawconstr 
+  -> unsafe_type_judgment
+
+(* To embed constr in rawconstr *)
+val constr_in : constr -> Dyn.t
+val constr_out : Dyn.t -> constr
+
+(*i*)
+(* Internal of Pretyping...
+ * Unused outside, but useful for debugging
+ *)
+val pretype : 
+  type_constraint -> env -> evar_defs -> 
+    var_map * (identifier * identifier option) list ->
+    rawconstr -> unsafe_judgment
+
+val pretype_type : 
+  val_constraint -> env -> evar_defs ->
+    var_map * (identifier * identifier option) list ->
+    rawconstr -> unsafe_type_judgment
+(*i*)
+
+val interp_sort : rawsort -> sorts
+
+val interp_elimination_sort : rawsort -> sorts_family