diff options
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 864768fe5..ee568fbc4 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -12,7 +12,6 @@ into elementary ones, insertion of coercions and resolution of implicit arguments. *) -open Constr open Environ open Evd open EConstr @@ -26,7 +25,7 @@ val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> (** An auxiliary function for searching for fixpoint guard indexes *) val search_guard : - ?loc:Loc.t -> env -> int list list -> rec_declaration -> int array + ?loc:Loc.t -> env -> int list list -> Constr.rec_declaration -> int array type typing_constraint = OfType of types | IsType | WithoutTypeConstraint @@ -85,9 +84,8 @@ val understand_ltac : inference_flags -> heuristics (but no external tactic solver hook), as well as to ensure that conversion problems are all solved and that no unresolved evar remains, expanding evars. *) - val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> - env -> evar_map -> glob_constr -> Constr.constr Evd.in_evar_universe_context + env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context (** Trying to solve remaining evars and remaining conversion problems possibly using type classes, heuristics, external tactic solver |