Fixing bug #2724 (using notations with binders in cases patterns

was provoking an anomaly instead of a regular error).

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

5 files changed, 43 insertions, 16 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6b221ecd87..3890931274 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -868,9 +868,6 @@ let message_redundant_alias (id1,id2) =
 
 (* Expanding notations *)
 
-let error_invalid_pattern_notation loc =
-  user_err_loc (loc,"",str "Invalid notation for pattern.")
-
 let rec subst_pat_iterator y t (subst,p) = match p with
   | PatVar (_,id) as x ->
       if id = Name y then t else [subst,x]
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index db41809628..8db5b0afa2 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -924,7 +924,7 @@ let oldfashion_patterns = ref (true)
 let write_oldfashion_patterns = Goptions.declare_bool_option {
   Goptions.optsync = true; Goptions.optdepr = false;
   Goptions.optname =
-    "Constructors in atterns require all their arguments but no parameters instead of explicit parameters and arguments";
+    "Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments";
   Goptions.optkey = ["Asymmetric";"Patterns"];
   Goptions.optread = (fun () -> !oldfashion_patterns);
   Goptions.optwrite = (fun a -> oldfashion_patterns:=a);
@@ -942,6 +942,12 @@ let names_of_local_binders bl =
   List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
 
 (**********************************************************************)
+(* Miscellaneous *)
+
+let error_invalid_pattern_notation loc =
+  user_err_loc (loc,"",str "Invalid notation for pattern.")
+
+(**********************************************************************)
 (* Functions on constr_expr *)
 
 let constr_loc = function
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 337eb00472..b346655ad7 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -270,3 +270,7 @@ val ntn_loc :
   loc -> constr_notation_substitution -> string -> (int * int) list
 val patntn_loc :
   loc -> cases_pattern_notation_substitution -> string -> (int * int) list
+
+(** For cases pattern parsing errors *)
+
+val error_invalid_pattern_notation : Pp.loc -> 'a
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index ecd7a1acc4..17a4d98ad1 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -107,11 +107,14 @@ let make_constr_action
   in
   make ([],[],[]) (List.rev pil)
 
+let check_cases_pattern_env loc (env,envlist,hasbinders) =
+  if hasbinders then error_invalid_pattern_notation loc else (env,envlist)
+
 let make_cases_pattern_action
   (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
-  let rec make (env,envlist as fullenv) = function
+  let rec make (env,envlist,hasbinders as fullenv) = function
   | [] ->
-      Gram.action (fun loc -> f loc fullenv)
+      Gram.action (fun loc -> f loc (check_cases_pattern_env loc fullenv))
   | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
       (* parse a non-binding item *)
       Gram.action (fun _ -> make fullenv tl)
@@ -119,28 +122,37 @@ let make_cases_pattern_action
       (* parse a binding non-terminal *)
     (match typ with
     | ETConstr _ -> (* pattern non-terminal *)
-        Gram.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl)
+        Gram.action (fun (v:cases_pattern_expr) ->
+          make (v::env, envlist, hasbinders) tl)
     | ETReference ->
         Gram.action (fun (v:reference) ->
-	  make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl)
+	  make (CPatAtom (dummy_loc,Some v) :: env, envlist, hasbinders) tl)
     | ETName ->
         Gram.action (fun (na:name located) ->
-	  make (cases_pattern_expr_of_name na :: env, envlist) tl)
+	  make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl)
     | ETBigint ->
         Gram.action (fun (v:Bigint.bigint) ->
-	  make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl)
+	  make (CPatPrim (dummy_loc,Numeral v) :: env, envlist, hasbinders) tl)
     | ETConstrList (_,_) ->
         Gram.action  (fun (vl:cases_pattern_expr list) ->
-	  make (env, vl :: envlist) tl)
-    | (ETPattern | ETBinderList _ | ETBinder _ | ETOther _) ->
-	failwith "Unexpected entry of type cases pattern or other")
+	  make (env, vl :: envlist, hasbinders) tl)
+    | ETBinder _ | ETBinderList (true,_) ->
+	Gram.action (fun (v:local_binder list) ->
+	  make (env, envlist, hasbinders) tl)
+    | ETBinderList (false,_) ->
+	Gram.action (fun (v:local_binder list list) ->
+	  make (env, envlist, true) tl)
+    | (ETPattern | ETOther _) ->
+        anomaly "Unexpected entry of type cases pattern or other")
   | GramConstrListMark (n,b) :: tl ->
       (* Rebuild expansions of ConstrList *)
       let heads,env = list_chop n env in
-      if b then make (env,(heads@List.hd envlist)::List.tl envlist) tl
-      else make (env,heads::envlist) tl
+      if b then
+        make (env,(heads@List.hd envlist)::List.tl envlist,hasbinders) tl
+      else
+        make (env,heads::envlist,hasbinders) tl
   in
-  make ([],[]) (List.rev pil)
+  make ([],[],false) (List.rev pil)
 
 let rec make_constr_prod_item assoc from forpat = function
   | GramConstrTerminal tok :: l ->
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index f5f5a9d14c..3c34ff9289 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -86,3 +86,11 @@ Notation "'FOO' x" := (S x) (at level 40).
 Goal (2 ++++ 3) = 5.
 reflexivity.
 Abort.
+
+(* Check correct failure handling when a non-constructor notation is
+   used in cases pattern (bug #2724 in 8.3 and 8.4beta) *)
+
+Notation "'FORALL'  x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity) : type_scope.
+
+Fail Check fun x => match x with S (FORALL x, _) => 0 end.