diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index bf62cea6b..3757ba7e6 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -23,7 +23,6 @@ open Evardefine open Evarsolve open Evd open Pretype_errors -open Sigma.Notations open Context.Named.Declaration module RelDecl = Context.Rel.Declaration @@ -638,7 +637,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in - let na = Nameops.name_max na1 na2 in + let na = Nameops.Name.pick na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = @@ -755,7 +754,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.name_max na1 na2 in + let na = Nameops.Name.pick na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 @@ -816,7 +815,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.name_max n1 n2 in + let na = Nameops.Name.pick n1 n2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> @@ -913,9 +912,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (i,t2::ks, m-1, test) else let dloc = Loc.tag Evar_kinds.InternalHole in - let i = Sigma.Unsafe.of_evar_map i in - let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in - let i' = Sigma.to_evar_map i' in + let (i', ev) = Evarutil.new_evar env i ~src:dloc (substl ks b) in (i', ev :: ks, m - 1,test)) (evd,[],List.length bs,fun i -> Success i) bs in @@ -1088,7 +1085,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let filter' = filter_possible_projections evd c ty ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) | _, _, [] -> [] - | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in + | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") in let rec set_holes evdref rhs = function | (id,_,c,cty,evsref,filter,occs)::subst -> @@ -1099,9 +1096,8 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | None -> let evty = set_holes evdref cty subst in let instance = Filter.filter_list filter instance in - let evd = Sigma.Unsafe.of_evar_map !evdref in - let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in - let evd = Sigma.to_evar_map evd in + let evd = !evdref in + let (evd, ev) = new_evar_instance sign evd evty ~filter instance in evdref := evd; evsref := (fst (destEvar !evdref ev),evty)::!evsref; ev in |