diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/inductiveops.ml | 7 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 3 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 6 |
4 files changed, 8 insertions, 10 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 275a079d5..33d674ff5 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -643,8 +643,9 @@ let type_of_projection_knowing_arg env sigma p c ty = (* A function which checks that a term well typed verifies both syntactic conditions *) -let control_only_guard env c = - let check_fix_cofix e c = match kind c with +let control_only_guard env sigma c = + let check_fix_cofix e c = + match kind (EConstr.to_constr sigma c) with | CoFix (_,(_,_,_) as cofix) -> Inductive.check_cofix e cofix | Fix (_,(_,_,_) as fix) -> @@ -653,6 +654,6 @@ let control_only_guard env c = in let rec iter env c = check_fix_cofix env c; - iter_constr_with_full_binders push_rel iter env c + iter_constr_with_full_binders sigma EConstr.push_rel iter env c in iter env c diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 55149552a..8efa087a7 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -198,4 +198,4 @@ val type_of_inductive_knowing_conclusion : env -> evar_map -> Inductive.mind_specif Univ.puniverses -> EConstr.types -> evar_map * EConstr.types (********************) -val control_only_guard : env -> types -> unit +val control_only_guard : env -> Evd.evar_map -> EConstr.types -> unit diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6700748eb..79d255b0b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1205,8 +1205,7 @@ let all_no_fail_flags = default_inference_flags false let ise_pretype_gen_ctx flags env sigma lvar kind c = let evd, c, _ = ise_pretype_gen flags env sigma lvar kind c in - let evd, f = Evarutil.nf_evars_and_universes evd in - f (EConstr.Unsafe.to_constr c), Evd.evar_universe_context evd + c, Evd.evar_universe_context evd (** Entry points of the high-level type synthesis algorithm *) 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 |