diff options
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index ec8aae140..79b051845 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -81,14 +81,16 @@ val understand_ltac : inference_flags -> (** Standard call to get a constr from a glob_constr, resolving implicit args *) val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> - evar_map -> env -> glob_constr -> constr + evar_map -> env -> glob_constr -> constr Univ.in_universe_context_set (** Idem but returns the judgment of the understood term *) -val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment +val understand_judgment : evar_map -> env -> + glob_constr -> unsafe_judgment Evd.in_evar_universe_context (** Idem but do not fail on unresolved evars *) -val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment +val understand_judgment_tcc : evar_map ref -> env -> + glob_constr -> unsafe_judgment (** Trying to solve remaining evars and remaining conversion problems with type classes, heuristics, and possibly an external solver *) @@ -122,7 +124,7 @@ val ise_pretype_gen : val constr_in : constr -> Dyn.t val constr_out : Dyn.t -> constr -val interp_sort : glob_sort -> sorts +val interp_sort : evar_map -> glob_sort -> evar_map * sorts val interp_elimination_sort : glob_sort -> sorts_family val genarg_interp_hook : |