diff options
| author | Pierre-Marie Pédrot | 2019-12-18 16:52:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-18 16:52:10 +0100 |
| commit | dfdfa9eeedebb0aec2cd72be9c1eee27ca9b2fab (patch) | |
| tree | c6e4c772dae91a047c488f20fb3b03afd384300a /pretyping | |
| parent | 6b9f6c365ec5b478e79f70cf2a1ae4faed809b74 (diff) | |
| parent | 467d4f28802bf07bb0cdb748c78f0936219ceb8d (diff) | |
Merge PR #11027: Cleanup post #10647 (expose comind universe handling)
Reviewed-by: ppedrot
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 16 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 7 |
2 files changed, 13 insertions, 10 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4925f3e5fa..44b3d59287 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -288,16 +288,18 @@ let check_extra_evars_are_solved env current_sigma frozen = match frozen with (* [check_evars] fails if some unresolved evar remains *) -let check_evars env initial_sigma sigma c = +let check_evars env ?initial sigma c = let rec proc_rec c = match EConstr.kind sigma c with | Evar (evk, _) -> - if not (Evd.mem initial_sigma evk) then - let (loc,k) = evar_source evk sigma in - begin match k with - | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () - | _ -> Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None - end + (match initial with + | Some initial when Evd.mem initial evk -> () + | _ -> + let (loc,k) = evar_source evk sigma in + begin match k with + | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () + | _ -> Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None + end) | _ -> EConstr.iter sigma proc_rec c in proc_rec c diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index f9da568c75..4aaf1376ad 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -115,9 +115,10 @@ val solve_remaining_evars : ?hook:inference_hook -> inference_flags -> val check_evars_are_solved : program_mode:bool -> env -> ?initial:evar_map -> (* current map: *) evar_map -> unit -(** [check_evars env initial_sigma extended_sigma c] fails if some - new unresolved evar remains in [c] *) -val check_evars : env -> evar_map -> evar_map -> constr -> unit +(** [check_evars env ?initial sigma c] fails if some unresolved evar + remains in [c] which isn't in [initial] (any unresolved evar if + [initial] not provided) *) +val check_evars : env -> ?initial:evar_map -> evar_map -> constr -> unit (**/**) (** Internal of Pretyping... *) |