- Correction filtrage des notations impliquant un "match" : la présence

  des localisations empêchait toute unification des pattern de filtrage
  de réussir.
- Ajout au passage d'unification des pattern modulo alpha.
- Exemples dans Notations.v


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9163 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 4 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 06a8ec9d0..c613bf0db 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -394,6 +394,15 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
 
+let rec match_cases_pattern metas acc pat1 pat2 =
+  match (pat1,pat2) with
+  | PatVar (_,na1), PatVar (_,na2) -> match_names metas acc na1 na2
+  | PatCstr (_,c1,patl1,na1), PatCstr (_,c2,patl2,na2)
+      when c1 = c2 & List.length patl1 = List.length patl2 ->
+      List.fold_left2 (match_cases_pattern metas)
+	(match_names metas acc na1 na2) patl1 patl2
+  | _ -> raise No_match
+
 let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1
   | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
@@ -462,10 +471,12 @@ and match_binders alp metas na1 na2 sigma b1 b2 =
   let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
   match_ alp metas sigma b1 b2
 
-and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) =
-  if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then
-    match_ alp metas sigma rhs1 rhs2
-  else raise No_match
+and match_equations alp metas sigma (_,_,patl1,rhs1) (_,patl2,rhs2) =
+  (* patl1 and patl2 have the same length because they respectively
+     correspond to some tml1 and tml2 that have the same length *)
+  let (alp,sigma) = 
+    List.fold_left2 (match_cases_pattern metas) (alp,sigma) patl1 patl2 in
+  match_ alp metas sigma rhs1 rhs2
 
 type scope_name = string