diff options
| author | delahaye | 2000-05-03 17:31:07 +0000 |
|---|---|---|
| committer | delahaye | 2000-05-03 17:31:07 +0000 |
| commit | fc38a7d8f3d2a47aa8eee570747568335f3ffa19 (patch) | |
| tree | 9ddc595a02cf1baaab3e9595d77b0103c80d66bf /proofs/pattern.ml | |
| parent | 5b0f516e7e1f6d2ea8ca0485ffe347a613b01a5c (diff) | |
Ajout du langage de tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |