diff options
| -rw-r--r-- | pretyping/coercion.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 16 | ||||
| -rw-r--r-- | pretyping/evd.ml | 15 | ||||
| -rw-r--r-- | pretyping/evd.mli | 6 |
4 files changed, 10 insertions, 29 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index e97e45580..70fc659cb 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -377,7 +377,7 @@ let inh_coerce_to_sort loc env evd j = let typ = whd_betadeltaiota env evd j.uj_type in match kind_of_term typ with | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s }) - | Evar ev when not (is_defined_evar evd ev) -> + | Evar ev when not (is_defined evd (fst ev)) -> let (evd',s) = define_evar_as_sort evd ev in (evd',{ utj_val = j.uj_val; utj_type = s }) | _ -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 39e262a3c..f859d0b42 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -257,16 +257,18 @@ let rec evar_conv_x ts env evd pbty term1 term2 = destroy beta-redexes that can be used for 1st-order unification *) let term1 = apprec_nohdbeta ts env evd term1 in let term2 = apprec_nohdbeta ts env evd term2 in - if is_undefined_evar evd term1 then + begin match kind_of_term term1, kind_of_term term2 with + | Evar ev, _ when Evd.is_undefined evd (fst ev) -> solve_simple_eqn (evar_conv_x ts) env evd - (position_problem true pbty,destEvar term1,term2) - else if is_undefined_evar evd term2 then + (position_problem true pbty,ev,term2) + | _, Evar ev when Evd.is_undefined evd (fst ev) -> solve_simple_eqn (evar_conv_x ts) env evd - (position_problem false pbty,destEvar term2,term1) - else + (position_problem false pbty,ev,term1) + | _ -> evar_eqappr_x ts env evd pbty (whd_nored_state evd (term1,empty_stack), Cst_stack.empty) - (whd_nored_state evd (term2,empty_stack), Cst_stack.empty) + (whd_nored_state evd (term2,empty_stack), Cst_stack.empty) + end and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) = @@ -617,7 +619,7 @@ let first_order_unification ts env evd (ev1,l1) (term2,l2) = (fun i -> (* Then instantiate evar unless already done by unifying args *) let t2 = applist(term2,deb2) in - if is_defined_evar i ev1 then + if is_defined i (fst ev1) then evar_conv_x ts env i CONV t2 (mkEvar ev1) else solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1,t2))] diff --git a/pretyping/evd.ml b/pretyping/evd.ml index cc525dca1..6f56f1bfa 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -450,13 +450,6 @@ let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter evar_candidates = candidates; evar_extra = Store.empty } } -let is_defined_evar evd (evk,_) = EvarMap.is_defined evd.evars evk - -(* Does k corresponds to an (un)defined existential ? *) -let is_undefined_evar evd c = match kind_of_term c with - | Evar ev -> not (is_defined_evar evd ev) - | _ -> false - (* extracts conversion problems that satisfy predicate p *) (* Note: conv_pbs not satisying p are stored back in reverse order *) let extract_conv_pbs evd p = @@ -585,8 +578,6 @@ let set_eq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 = let meta_list evd = metamap_to_list evd.metas -let find_meta evd mv = Metamap.find mv evd.metas - let undefined_metas evd = let filter = function | (n,Clval(_,_,typ)) -> None @@ -595,12 +586,6 @@ let undefined_metas evd = let m = List.map_filter filter (meta_list evd) in List.sort (-) m -let metas_of evd = - List.map (function - | (n,Clval(_,_,typ)) -> (n,typ.rebus) - | (n,Cltyp (_,typ)) -> (n,typ.rebus)) - (meta_list evd) - let map_metas_fvalue f evd = { evd with metas = Metamap.map diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 49878ce8a..d3155201d 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -172,9 +172,6 @@ val subst_evar_defs_light : substitution -> evar_map -> evar_map val evars_reset_evd : ?with_conv_pbs:bool -> evar_map -> evar_map -> evar_map -(* spiwack: [is_undefined_evar] should be considered a candidate - for moving to evarutils *) -val is_undefined_evar : evar_map -> constr -> bool val undefined_evars : evar_map -> evar_map val defined_evars : evar_map -> evar_map (* [fold_undefined f m] iterates ("folds") function [f] over the undefined @@ -207,7 +204,6 @@ val evar_list : evar_map -> constr -> existential list val collect_evars : constr -> ExistentialSet.t (** Metas *) -val find_meta : evar_map -> metavariable -> clbinding val meta_list : evar_map -> (metavariable * clbinding) list val meta_defined : evar_map -> metavariable -> bool @@ -229,7 +225,6 @@ val meta_reassign : metavariable -> constr * instance_status -> evar_map -> eva val meta_merge : evar_map -> evar_map -> evar_map val undefined_metas : evar_map -> metavariable list -val metas_of : evar_map -> meta_type_map val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map type metabinding = metavariable * constr * instance_status @@ -279,6 +274,5 @@ val pr_metaset : Metaset.t -> Pp.std_ppcmds create an [evar_map] with empty meta map: *) val create_evar_defs : evar_map -> evar_map val create_goal_evar_defs : evar_map -> evar_map -val is_defined_evar : evar_map -> existential -> bool val subst_evar_map : substitution -> evar_map -> evar_map (*** /Deprecaded ***) |