3 files changed, 39 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
 
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 3ab3de457..d26051758 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -22,3 +22,13 @@ forall n : nat, n = 0
      : list nat
 (1; 2, 4)
      : nat * nat * nat
+Defining 'ifzero' as keyword
+ifzero 3
+     : bool
+Defining 'pred' as keyword
+pred 3
+     : nat
+fun n : nat => pred n
+     : nat -> nat
+fun n : nat => pred n
+     : nat -> nat
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 4382975e8..5330e145e 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -17,12 +17,16 @@ Check (decomp (true,true) as t, u in (t,u)).
 (**********************************************************************)
 (* Behaviour wrt to binding variables (submitted by Roland Zumkeller) *)
 
+Section A.
+
 Notation "! A" := (forall _:nat, A) (at level 60).
 
 Check ! (0=0).
 Check forall n, n=0.
 Check forall n:nat, 0=0.
 
+End A.
+
 (**********************************************************************)
 (* Conflict between notation and notation below coercions             *)
 
@@ -66,3 +70,13 @@ Check [1;2;4].
 Reserved Notation "( x ; y , .. , z )" (at level 0).
 Notation "( x ; y , .. , z )" := (pair .. (pair x y) .. z).
 Check (1;2,4).
+
+Notation "'ifzero' n" := (match n with 0 => true | S _ => false end)
+  (at level 0, n at level 0).
+Check (ifzero 3).
+
+Notation "'pred' n" := (match n with 0 => 0 | S n' => n' end)
+  (at level 0, n at level 0).
+Check (pred 3).
+Check (fun n => match n with 0 => 0 | S n => n end).
+Check (fun n => match n with S p as x => p | y => 0 end).