diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/evd.ml | 44 | ||||
| -rw-r--r-- | kernel/evd.mli | 14 |
2 files changed, 25 insertions, 33 deletions
diff --git a/kernel/evd.ml b/kernel/evd.ml index 5836f7775c..9295d35872 100644 --- a/kernel/evd.ml +++ b/kernel/evd.ml @@ -19,53 +19,45 @@ type evar_body = | Evar_defined of constr type evar_info = { - evar_concl : typed_type; (* the type of the evar ... *) - evar_hyps : typed_type signature; (* ... under a certain signature *) - evar_body : evar_body } (* any other necessary information *) + evar_concl : constr; + evar_hyps : typed_type signature; + evar_body : evar_body } type evar_map = evar_info Intmap.t let mt_evd = Intmap.empty -let to_list evc = Intmap.fold (fun sp x acc -> (sp,x)::acc) evc [] -let dom evc = Intmap.fold (fun sp _ acc -> sp::acc) evc [] +let to_list evc = Intmap.fold (fun ev x acc -> (ev,x)::acc) evc [] +let dom evc = Intmap.fold (fun ev _ acc -> ev::acc) evc [] let map evc k = Intmap.find k evc let rmv evc k = Intmap.remove k evc let remap evc k i = Intmap.add k i evc let in_dom evc k = Intmap.mem k evc -let add_with_info evd sp newinfo = - Intmap.add sp newinfo evd +let add evd ev newinfo = Intmap.add ev newinfo evd -let add_noinfo evd sp sign typ = - let newinfo = - { evar_concl = typ; - evar_hyps = sign; - evar_body = Evar_empty } - in - Intmap.add sp newinfo evd - -let define evd sp body = - let oldinfo = map evd sp in +let define evd ev body = + let oldinfo = map evd ev in let newinfo = { evar_concl = oldinfo.evar_concl; - evar_hyps = oldinfo.evar_hyps; - evar_body = Evar_defined body } + evar_hyps = oldinfo.evar_hyps; + evar_body = Evar_defined body } in match oldinfo.evar_body with - | Evar_empty -> Intmap.add sp newinfo evd + | Evar_empty -> Intmap.add ev newinfo evd | _ -> anomaly "cannot define an isevar twice" (* The list of non-instantiated existential declarations *) let non_instantiated sigma = - let listsp = to_list sigma in + let listev = to_list sigma in List.fold_left - (fun l ((sp,evd) as d) -> + (fun l ((ev,evd) as d) -> if evd.evar_body = Evar_empty then (d::l) else l) - [] listsp + [] listev -let is_evar sigma sp = in_dom sigma sp +let is_evar sigma ev = in_dom sigma ev -let is_defined sigma sp = - let info = map sigma sp in not (info.evar_body = Evar_empty) +let is_defined sigma ev = + let info = map sigma ev in + not (info.evar_body = Evar_empty) diff --git a/kernel/evd.mli b/kernel/evd.mli index fa60292836..89cefcab11 100644 --- a/kernel/evd.mli +++ b/kernel/evd.mli @@ -10,7 +10,8 @@ open Sign (* The type of mappings for existential variables. The keys are integers and the associated information is a record containing the type of the evar ([concl]), the signature under which - it was introduced ([hyps]) and its definition ([body]). *) + it was introduced ([hyps]) and its definition ([body]). + [evar_info] is used to add any other kind of information. *) type evar = int @@ -21,12 +22,14 @@ type evar_body = | Evar_defined of constr type evar_info = { - evar_concl : typed_type; - evar_hyps : typed_type signature; - evar_body : evar_body } + evar_concl : constr; + evar_hyps : typed_type signature; + evar_body : evar_body } type evar_map +val add : evar_map -> evar -> evar_info -> evar_map + val dom : evar_map -> evar list val map : evar_map -> evar -> evar_info val rmv : evar_map -> evar -> evar_map @@ -35,9 +38,6 @@ val in_dom : evar_map -> evar -> bool val to_list : evar_map -> (evar * evar_info) list val mt_evd : evar_map -val add_with_info : evar_map -> evar -> evar_info -> evar_map -val add_noinfo : - evar_map -> evar -> typed_type signature -> typed_type -> evar_map val define : evar_map -> evar -> constr -> evar_map |