diff options
| author | aspiwack | 2011-05-13 17:57:57 +0000 |
|---|---|---|
| committer | aspiwack | 2011-05-13 17:57:57 +0000 |
| commit | aaafa92638be941a8750b1d88f42be69b807e550 (patch) | |
| tree | b62b176333792637e81653fcfb69dd395fe6e731 | |
| parent | 74158af19fc897734454f97e109d08be7ff6fc59 (diff) | |
A better procedure for checking presence of undefined evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14121 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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. *) |