diff options
Diffstat (limited to 'pretyping/constr_matching.ml')
| -rw-r--r-- | pretyping/constr_matching.ml | 39 |
1 files changed, 20 insertions, 19 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index ee3c43d8..886a9826 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -8,7 +8,7 @@ (*i*) open Pp -open Errors +open CErrors open Util open Names open Globnames @@ -17,10 +17,10 @@ open Termops open Reductionops open Term open Vars -open Context open Pattern open Patternops open Misctypes +open Context.Rel.Declaration (*i*) (* Given a term with second-order variables in it, @@ -49,12 +49,12 @@ type bound_ident_map = Id.t Id.Map.t exception PatternMatchingFailure -let warn_bound_meta name = - msg_warning (str "Collision between bound variable " ++ pr_id name ++ - str " and a metavariable of same name.") +let warn_meta_collision = + CWarnings.create ~name:"meta-collision" ~category:"ltac" + (fun name -> + strbrk "Collision between bound variable " ++ pr_id name ++ + strbrk " and a metavariable of same name.") -let warn_bound_bound name = - msg_warning (str "Collision between bound variables of name " ++ pr_id name) let constrain n (ids, m as x) (names, terms as subst) = try @@ -62,18 +62,19 @@ let constrain n (ids, m as x) (names, terms as subst) = if List.equal Id.equal ids ids' && eq_constr m m' then subst else raise PatternMatchingFailure with Not_found -> - let () = if Id.Map.mem n names then warn_bound_meta n in + let () = if Id.Map.mem n names then warn_meta_collision n in (names, Id.Map.add n x terms) let add_binders na1 na2 binding_vars (names, terms as subst) = match na1, na2 with | Name id1, Name id2 when Id.Set.mem id1 binding_vars -> if Id.Map.mem id1 names then - let () = warn_bound_bound id1 in + let () = Glob_ops.warn_variable_collision id1 in (names, terms) else let names = Id.Map.add id1 id2 names in - let () = if Id.Map.mem id1 terms then warn_bound_meta id1 in + let () = if Id.Map.mem id1 terms then + warn_meta_collision id1 in (names, terms) | _ -> subst @@ -255,24 +256,24 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels sorec ctx env subst c1 c2 | PProd (na1,c1,d1), Prod(na2,c2,d2) -> - sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env) + sorec ((na1,na2,c2)::ctx) (Environ.push_rel (LocalAssum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PLambda (na1,c1,d1), Lambda(na2,c2,d2) -> - sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env) + sorec ((na1,na2,c2)::ctx) (Environ.push_rel (LocalAssum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) -> - sorec ((na1,na2,t2)::ctx) (Environ.push_rel (na2,Some c2,t2) env) + sorec ((na1,na2,t2)::ctx) (Environ.push_rel (LocalDef (na2,c2,t2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> let ctx_b2,b2 = decompose_lam_n_decls ci.ci_cstr_ndecls.(0) b2 in let ctx_b2',b2' = decompose_lam_n_decls ci.ci_cstr_ndecls.(1) b2' in - let n = rel_context_length ctx_b2 in - let n' = rel_context_length ctx_b2' in + let n = Context.Rel.length ctx_b2 in + let n' = Context.Rel.length ctx_b2' in if noccur_between 1 n b2 && noccur_between 1 n' b2' then - let f l (na,_,t) = (Anonymous,na,t)::l in + let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = (Anonymous,na,t)::l in let ctx_br = List.fold_left f ctx ctx_b2 in let ctx_br' = List.fold_left f ctx ctx_b2' in let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in @@ -368,21 +369,21 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2)) | _ -> assert false in - let env' = Environ.push_rel (x,None,c1) env in + let env' = Environ.push_rel (LocalAssum (x,c1)) env in try_aux [(env, c1); (env', c2)] next_mk_ctx next | Prod (x,c1,c2) -> let next_mk_ctx = function | [c1; c2] -> mk_ctx (mkProd (x, c1, c2)) | _ -> assert false in - let env' = Environ.push_rel (x,None,c1) env in + let env' = Environ.push_rel (LocalAssum (x,c1)) env in try_aux [(env, c1); (env', c2)] next_mk_ctx next | LetIn (x,c1,t,c2) -> let next_mk_ctx = function | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2)) | _ -> assert false in - let env' = Environ.push_rel (x,Some c1,t) env in + let env' = Environ.push_rel (LocalDef (x,c1,t)) env in try_aux [(env, c1); (env', c2)] next_mk_ctx next | App (c1,lc) -> let topdown = true in |