diff options
Diffstat (limited to 'proofs/pattern.ml')
| -rw-r--r-- | proofs/pattern.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/proofs/pattern.ml b/proofs/pattern.ml index a30a829927..983154c80f 100644 --- a/proofs/pattern.ml +++ b/proofs/pattern.ml @@ -100,9 +100,12 @@ let head_of_constr_reference = function *) +exception PatternMatchingFailure + let constrain ((n : int),(m : constr)) sigma = if List.mem_assoc n sigma then - if eq_constr m (List.assoc n sigma) then sigma else error "somatch" + if eq_constr m (List.assoc n sigma) then sigma + else raise PatternMatchingFailure else (n,m)::sigma @@ -124,8 +127,6 @@ let memb_metavars m n = let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2 -exception PatternMatchingFailure - let matches_core convert pat c = let rec sorec stk sigma p t = let cT = whd_castapp t in @@ -180,6 +181,9 @@ let matches_core convert pat c = | PBinder(BLambda,na1,c1,d1), IsLambda(na2,c2,d2) -> sorec (na2::stk) (sorec stk sigma c1 c2) d1 d2 + | PRef (RConst (sp1,ctxt1)), IsConst (sp2,ctxt2) + when sp1 = sp2 && eq_context ctxt1 ctxt2 -> sigma + | PRef (RConst (sp1,ctxt1)), _ when convert <> None -> let (env,evars) = out_some convert in if is_conv env evars (mkConst (sp1,ctxt1)) cT then sigma |