diff options
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 142b54513..a6aa08657 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -123,11 +123,11 @@ val check_evars_are_solved : (**/**) (** Internal of Pretyping... *) val pretype : - bool -> type_constraint -> env -> evar_map ref -> + int -> bool -> type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment val pretype_type : - bool -> val_constraint -> env -> evar_map ref -> + int -> bool -> val_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_type_judgment val ise_pretype_gen : |