diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-02-14 19:23:02 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-02-19 17:46:50 +0100 |
| commit | ef09beee5057251ce066e05be2fa118abc8d09e9 (patch) | |
| tree | 5f022b98746592c27dd8cc7fa1c66fe8f0415f8b /pretyping/pretyping.mli | |
| parent | aec63ba9c8f6840d98ba731640a786138d836343 (diff) | |
pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index fe10be9e7..864768fe5 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -58,6 +58,11 @@ val all_and_fail_flags : inference_flags val understand_tcc : ?flags:inference_flags -> env -> evar_map -> ?expected_type:typing_constraint -> glob_constr -> evar_map * constr +(** As [understand_tcc] but also returns the type of the elaborated term. + The [expand_evars] flag is not applied to the type (only to the term). *) +val understand_tcc_ty : ?flags:inference_flags -> env -> evar_map -> + ?expected_type:typing_constraint -> glob_constr -> evar_map * constr * types + (** More general entry point with evars from ltac *) (** Generic call to the interpreter from glob_constr to constr @@ -116,7 +121,7 @@ val pretype_type : val ise_pretype_gen : inference_flags -> env -> evar_map -> - ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr + ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr * types (**/**) |