diff options
Diffstat (limited to 'kernel/evd.ml')
| -rw-r--r-- | kernel/evd.ml | 48 |
1 files changed, 24 insertions, 24 deletions
diff --git a/kernel/evd.ml b/kernel/evd.ml index 77351ab9b7..5b870d87af 100644 --- a/kernel/evd.ml +++ b/kernel/evd.ml @@ -12,11 +12,10 @@ type evar_body = EVAR_EMPTY | EVAR_DEFINED of constr type 'a evar_info = { - concl : constr; (* the type of the evar ... *) - hyps : context; (* ... under a certain signature *) - body : evar_body; (* its definition *) - info : 'a option (* any other necessary information *) -} + evar_concl : typed_type; (* the type of the evar ... *) + evar_hyps : context; (* ... under a certain signature *) + evar_body : evar_body; (* its definition *) + evar_info : 'a option } (* any other necessary information *) type 'a evar_map = 'a evar_info Spmap.t @@ -34,31 +33,32 @@ let add_with_info evd sp newinfo = let add_noinfo evd sp sign typ = let newinfo = - { concl = typ; - hyps = sign; - body = EVAR_EMPTY; - info = None} + { evar_concl = typ; + evar_hyps = sign; + evar_body = EVAR_EMPTY; + evar_info = None} in Spmap.add sp newinfo evd let define evd sp body = - let oldinfo = map evd sp in - let newinfo = - { concl = oldinfo.concl; - hyps = oldinfo.hyps; - body = EVAR_DEFINED body; - info = oldinfo.info} - in - match oldinfo.body with - | EVAR_EMPTY -> Spmap.add sp newinfo evd - | _ -> anomaly "cannot define an isevar twice" + let oldinfo = map evd sp in + let newinfo = + { evar_concl = oldinfo.evar_concl; + evar_hyps = oldinfo.evar_hyps; + evar_body = EVAR_DEFINED body; + evar_info = oldinfo.evar_info} + in + match oldinfo.evar_body with + | EVAR_EMPTY -> Spmap.add sp newinfo evd + | _ -> anomaly "cannot define an isevar twice" (* The list of non-instantiated existential declarations *) let non_instantiated sigma = - let listsp = toList sigma in - List.fold_left - (fun l ((sp,evd) as d) -> if evd.body = EVAR_EMPTY then (d::l) else l) - [] listsp - + let listsp = toList sigma in + List.fold_left + (fun l ((sp,evd) as d) -> + if evd.evar_body = EVAR_EMPTY then (d::l) else l) + [] listsp + let is_evar sigma sp = in_dom sigma sp |