From 680a5f0cac29ca68db8b28415a7759794e0e2f9d Mon Sep 17 00:00:00 2001
From: pboutill
Date: Mon, 7 Jan 2013 18:19:55 +0000
Subject: Fixup notation printing in patterns

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16117 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/notation_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 9dcd24127f..c0e83447f7 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -772,7 +772,7 @@ let rec match_cases_pattern metas sigma a1 a2 =
   | r1, NVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
   | PatVar (_,Anonymous), NHole _ -> sigma,(0,[])
   | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
-      sigma,(0,largs)
+      sigma,(0,add_patterns_for_params (fst r1) largs)
   | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2)
       when eq_constructor r1 r2 ->
       let l1 = add_patterns_for_params (fst r1) args1 in
-- 
cgit v1.2.3