diff options
| author | Gaëtan Gilbert | 2019-10-29 13:20:04 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-12-16 11:48:53 +0100 |
| commit | 62adf2b9e03afa212fcd8819226da068bf4a32b8 (patch) | |
| tree | f21b6feeec930f418c0a3302fb9c50bfc13c384d /pretyping | |
| parent | 1df9e71a1f9b0729a17d09e009add2e87fcde5ad (diff) | |
Pretyping.check_evars: make initial evar map optional
There are no users in Coq but maybe some plugin wants it so don't
completely remove it
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... *) |