diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 27 |
1 files changed, 14 insertions, 13 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index aeaaefef..506cd03f 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarutil.ml 8695 2006-04-10 16:33:52Z msozeau $ *) +(* $Id: evarutil.ml 8759 2006-04-28 12:24:14Z herbelin $ *) open Util open Pp @@ -35,7 +35,7 @@ exception Uninstantiated_evar of existential_key let rec whd_ise sigma c = match kind_of_term c with - | Evar (ev,args) when Evd.in_dom sigma ev -> + | Evar (ev,args) when Evd.mem sigma ev -> if Evd.is_defined sigma ev then whd_ise sigma (existential_value sigma (ev,args)) else raise (Uninstantiated_evar ev) @@ -46,7 +46,7 @@ let rec whd_ise sigma c = let whd_castappevar_stack sigma c = let rec whrec (c, l as s) = match kind_of_term c with - | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> + | Evar (ev,args) when Evd.mem sigma ev & Evd.is_defined sigma ev -> whrec (existential_value sigma (ev,args), l) | Cast (c,_,_) -> whrec (c, l) | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l) @@ -93,7 +93,7 @@ let collect_evars emap c = let rec collrec acc c = match kind_of_term c with | Evar (k,_) -> - if Evd.in_dom emap k & not (Evd.is_defined emap k) then k::acc + if Evd.mem emap k & not (Evd.is_defined emap k) then k::acc else (* No recursion on the evar instantiation *) acc | _ -> fold_constr collrec acc c in @@ -103,13 +103,14 @@ let push_dependent_evars sigma emap = Evd.fold (fun ev {evar_concl = ccl} (sigma',emap') -> List.fold_left (fun (sigma',emap') ev -> - (Evd.add sigma' ev (Evd.map emap' ev),Evd.rmv emap' ev)) + (Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev)) (sigma',emap') (collect_evars emap' ccl)) emap (sigma,emap) (* replaces a mapping of existentials into a mapping of metas. Problem if an evar appears in the type of another one (pops anomaly) *) let evars_to_metas sigma (emap, c) = + let emap = nf_evars emap in let sigma',emap' = push_dependent_evars sigma emap in let change_exist evar = let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in @@ -117,7 +118,7 @@ let evars_to_metas sigma (emap, c) = mkCast (mkMeta n, DEFAULTcast, ty) in let rec replace c = match kind_of_term c with - Evar (k,_ as ev) when Evd.in_dom emap' k -> change_exist ev + Evar (k,_ as ev) when Evd.mem emap' k -> change_exist ev | _ -> map_constr replace c in (sigma', replace c) @@ -209,7 +210,7 @@ let push_rel_context_to_named_context env = let id = next_name_away na avoid in ((mkVar id)::subst, id::avoid, - push_named (id,option_app (substl subst) c, + push_named (id,option_map (substl subst) c, type_app (substl subst) t) env)) (rel_context env) ~init:([],ids_of_named_context (named_context env),env) @@ -297,7 +298,7 @@ let is_defined_equation env evd (ev,inst) rhs = is_pattern inst && not (occur_evar ev rhs) && try - let evi = Evd.map (evars_of evd) ev in + let evi = Evd.find (evars_of evd) ev in let (evd',body) = inverse_instance env evd ev evi inst rhs in evar_well_typed_body evd' ev evi body with Failure _ -> false @@ -313,7 +314,7 @@ let is_defined_equation env evd (ev,inst) rhs = let do_restrict_hyps evd ev args = let args = Array.to_list args in - let evi = Evd.map (evars_of !evd) ev in + let evi = Evd.find (evars_of !evd) ev in let env = evar_env evi in let hyps = evar_context evi in let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in @@ -395,7 +396,7 @@ let evar_define env (ev,argsv) rhs isevars = if occur_evar ev rhs then error_occur_check env (evars_of isevars) ev rhs; let args = Array.to_list argsv in - let evi = Evd.map (evars_of isevars) ev in + let evi = Evd.find (evars_of isevars) ev in (* the bindings to invert *) let worklist = make_subst (evar_env evi) args in let (isevars',body) = real_clean env isevars ev evi worklist rhs in @@ -502,7 +503,7 @@ let status_changed lev (pbty,t1,t2) = let solve_refl conv_algo env isevars ev argsv1 argsv2 = if argsv1 = argsv2 then (isevars,[]) else - let evd = Evd.map (evars_of isevars) ev in + let evd = Evd.find (evars_of isevars) ev in let hyps = evar_context evd in let (isevars',_,rsign) = array_fold_left2 @@ -599,7 +600,7 @@ let mk_valcon c = Some c cumulativity now includes Prop and Set in Type... It is, but that's not too bad *) let define_evar_as_abstraction abs evd (ev,args) = - let evi = Evd.map (evars_of evd) ev in + let evi = Evd.find (evars_of evd) ev in let evenv = evar_env evi in let (evd1,dom) = new_evar evd evenv (new_Type()) in let nvar = @@ -679,7 +680,7 @@ let lift_abstr_tycon_type n (abs, t) = else (Some (init, abs'), t) let lift_tycon_type n (abs, t) = (abs, lift n t) -let lift_tycon n = option_app (lift_tycon_type n) +let lift_tycon n = option_map (lift_tycon_type n) let pr_tycon_type env (abs, t) = match abs with |