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 /pretyping | |
| 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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 6 | ||||
| -rw-r--r-- | pretyping/evd.mli | 3 |
2 files changed, 9 insertions, 0 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 |