diff options
| -rw-r--r-- | pretyping/evd.ml | 6 | ||||
| -rw-r--r-- | pretyping/evd.mli | 3 | ||||
| -rw-r--r-- | proofs/proofview.ml | 4 |
3 files changed, 10 insertions, 3 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index aa92481485..9d3e4225db 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -97,6 +97,8 @@ module EvarInfoMap = struct let empty = ExistentialMap.empty, ExistentialMap.empty + let has_undefined (_,u) = not (ExistentialMap.is_empty u) + let to_list (def,undef) = (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *) let l = ref [] in @@ -215,6 +217,7 @@ end module EvarMap = struct type t = EvarInfoMap.t * (Univ.UniverseLSet.t * Univ.universes) let empty = EvarInfoMap.empty, (Univ.UniverseLSet.empty, Univ.initial_universes) + let has_undefined (sigma,_) = EvarInfoMap.has_undefined sigma let add (sigma,sm) k v = (EvarInfoMap.add sigma k v, sm) let add_undefined (sigma,sm) k v = (EvarInfoMap.add_undefined sigma k v, sm) let find (sigma,_) = EvarInfoMap.find sigma @@ -416,6 +419,9 @@ let empty = { metas=Metamap.empty } +let has_undefined evd = + EvarMap.has_undefined evd.evars + let evars_reset_evd ?(with_conv_pbs=false) evd d = {d with evars = evd.evars; conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs } diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 3e14649b70..c0efdb9f82 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -142,6 +142,9 @@ val progress_evar_map : evar_map -> evar_map -> bool val empty : evar_map val is_empty : evar_map -> bool +(** [has_undefined sigma] is [true] if and only if + there are uninstantiated evars in [sigma]. *) +val has_undefined : evar_map -> bool val add : evar_map -> evar -> evar_info -> evar_map diff --git a/proofs/proofview.ml b/proofs/proofview.ml index aa00cee829..dd65a90495 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -467,9 +467,7 @@ module V82 = struct } let has_unresolved_evar pv = - let evd = pv.solution in - (* arnaud: essayer une procédure moins coûteuse *) - not ((Evarutil.non_instantiated evd) = []) + Evd.has_undefined pv.solution (* Returns the open goals of the proofview together with the evar_map to interprete them. *) |