From fc38a7d8f3d2a47aa8eee570747568335f3ffa19 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Wed, 3 May 2000 17:31:07 +0000
Subject: Ajout du langage de tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/pattern.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'proofs/pattern.ml')

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
-- 
cgit v1.2.3