diff options
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 35 |
1 files changed, 18 insertions, 17 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index e52112fda..622a8e982 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -18,7 +18,6 @@ open Constr open Glob_term open Pp open Mod_subst -open Misctypes open Decl_kinds open Pattern open Environ @@ -30,7 +29,7 @@ let case_info_pattern_eq i1 i2 = i1.cip_extensible == i2.cip_extensible let rec constr_pattern_eq p1 p2 = match p1, p2 with -| PRef r1, PRef r2 -> eq_gr r1 r2 +| PRef r1, PRef r2 -> GlobRef.equal r1 r2 | PVar v1, PVar v2 -> Id.equal v1 v2 | PEvar (ev1, ctx1), PEvar (ev2, ctx2) -> Evar.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2 @@ -47,7 +46,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with | PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) -> Name.equal v1 v2 && constr_pattern_eq b1 b2 && Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2 -| PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2 +| PSort s1, PSort s2 -> Glob_ops.glob_sort_eq s1 s2 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2 | PIf (t1, l1, r1), PIf (t2, l2, r2) -> constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2 @@ -184,7 +183,7 @@ let pattern_of_constr env sigma t = | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> (* These are the two evar kinds used for existing goals *) (* see Proofview.mark_in_evm *) - if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev) + if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value0 sigma ev) else PEvar (evk,Array.map (pattern_of_constr env) ctxt) | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false | _ -> @@ -279,9 +278,11 @@ let lift_pattern k = liftn_pattern k 1 let rec subst_pattern subst pat = match pat with | PRef ref -> - let ref',t = subst_global subst ref in - if ref' == ref then pat else - pattern_of_constr (Global.env()) Evd.empty t + let ref',t = subst_global subst ref in + if ref' == ref then pat else + let env = Global.env () in + let evd = Evd.from_env env in + pattern_of_constr env evd t | PVar _ | PEvar _ | PRel _ -> pat @@ -293,11 +294,11 @@ let rec subst_pattern subst pat = PProj(p',c') | PApp (f,args) -> let f' = subst_pattern subst f in - let args' = Array.smartmap (subst_pattern subst) args in + let args' = Array.Smart.map (subst_pattern subst) args in if f' == f && args' == args then pat else PApp (f',args') | PSoApp (i,args) -> - let args' = List.smartmap (subst_pattern subst) args in + let args' = List.Smart.map (subst_pattern subst) args in if args' == args then pat else PSoApp (i,args') | PLambda (name,c1,c2) -> @@ -312,7 +313,7 @@ let rec subst_pattern subst pat = PProd (name,c1',c2') | PLetIn (name,c1,t,c2) -> let c1' = subst_pattern subst c1 in - let t' = Option.smartmap (subst_pattern subst) t in + let t' = Option.Smart.map (subst_pattern subst) t in let c2' = subst_pattern subst c2 in if c1' == c1 && t' == t && c2' == c2 then pat else PLetIn (name,c1',t',c2') @@ -326,7 +327,7 @@ let rec subst_pattern subst pat = PIf (c',c1',c2') | PCase (cip,typ,c,branches) -> let ind = cip.cip_ind in - let ind' = Option.smartmap (subst_ind subst) ind in + let ind' = Option.Smart.map (subst_ind subst) ind in let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in let typ' = subst_pattern subst typ in let c' = subst_pattern subst c in @@ -334,18 +335,18 @@ let rec subst_pattern subst pat = let c' = subst_pattern subst c in if c' == c then br else (i,n,c') in - let branches' = List.smartmap subst_branch branches in + let branches' = List.Smart.map subst_branch branches in if cip' == cip && typ' == typ && c' == c && branches' == branches then pat else PCase(cip', typ', c', branches') | PFix (lni,(lna,tl,bl)) -> - let tl' = Array.smartmap (subst_pattern subst) tl in - let bl' = Array.smartmap (subst_pattern subst) bl in + let tl' = Array.Smart.map (subst_pattern subst) tl in + let bl' = Array.Smart.map (subst_pattern subst) bl in if bl' == bl && tl' == tl then pat else PFix (lni,(lna,tl',bl')) | PCoFix (ln,(lna,tl,bl)) -> - let tl' = Array.smartmap (subst_pattern subst) tl in - let bl' = Array.smartmap (subst_pattern subst) bl in + let tl' = Array.Smart.map (subst_pattern subst) tl in + let bl' = Array.Smart.map (subst_pattern subst) bl in if bl' == bl && tl' == tl then pat else PCoFix (ln,(lna,tl',bl')) @@ -416,7 +417,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (nal,(_,None),b,c) -> let mkGLambda na c = DAst.make ?loc @@ - GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in + GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None),c) in let c = List.fold_right mkGLambda nal c in let cip = { cip_style = LetStyle; |