Restructuration des points d'entrée de Pretyping et Constrintern

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

1 files changed, 28 insertions, 23 deletions

diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 80a9529c8a..d07b83ebac 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -18,49 +18,54 @@ open Rawterm
 open Evarutil
 (*i*)
 
+type typing_constraint = OfType of types option | IsType
+
+(* Generic call to the interpreter from rawconstr to open_constr, leaving
+   unresolved holes as evars and returning the typing contexts of
+   these evars. Work as [understand_gen] for the rest. *)
+
+val understand_tcc :
+  evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
+
+(* More general entry point with evars from ltac *)
+
 type var_map = (identifier * unsafe_judgment) list
 type unbound_ltac_var_map = (identifier * identifier option) list
 
 (* 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],
+   In [understand_ltac sigma env ltac_env constraint c],
 
    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)
+   ltac_env : partial substitution of variables (used for the tactic language)
+   constraint : tell if interpreted as a possibly constrained term or a type 
 *)
-val understand_gen :
-  evar_map -> env -> var_map
-    -> expected_type:(constr option) -> rawconstr -> constr
-
-(* Generic call to the interpreter from rawconstr to constr, leaving
-   unresolved holes as evars and returning the typing contexts of
-   these evars. Work as [understand_gen] for the rest. *)
-val understand_gen_tcc :
-  evar_map -> env -> var_map
-    -> expected_type:(constr option) -> rawconstr -> open_constr
 
-(* More general entry point with evars from ltac *)
-val understand_gen_ltac :
-  evar_map -> env -> var_map * unbound_ltac_var_map
-    -> expected_type:(constr option) -> rawconstr -> evar_defs * constr
+val understand_ltac :
+  evar_map -> env -> var_map * unbound_ltac_var_map ->
+    typing_constraint -> rawconstr -> evar_defs * constr
 
 (* Standard call to get a constr from a rawconstr, resolving implicit args *)
-val understand : evar_map -> env -> rawconstr -> constr
+
+val understand : evar_map -> env -> ?expected_type:Term.types ->
+  rawconstr -> constr
 
 (* Idem but the rawconstr is intended to be a type *)
+
 val understand_type : evar_map -> env -> rawconstr -> constr
 
+(* A generalization of the two previous case *)
+
+val understand_gen : typing_constraint -> 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
+val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
 
 (* To embed constr in rawconstr *)
+
 val constr_in : constr -> Dyn.t
 val constr_out : Dyn.t -> constr