Fixing Arguments Scope bug when too many scopes are given (bug #2667).

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

3 files changed, 19 insertions, 1 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b161d001d2..656baa9465 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -733,7 +733,7 @@ let apply_scope_env env = function
 
 let rec simple_adjust_scopes n = function
   | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
-  | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
+  | sc::scopes -> assert (n>0); sc :: simple_adjust_scopes (n-1) scopes
 
 let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
   let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
diff --git a/interp/notation.ml b/interp/notation.ml
index 8f19ab851f..9a88ad75d8 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -18,6 +18,7 @@ open Summary
 open Glob_term
 open Topconstr
 open Ppextend
+open Reductionops
 (*i*)
 
 (*s A scope is a set of notations; it includes
@@ -469,6 +470,17 @@ let compute_arguments_scope_full t =
 
 let compute_arguments_scope t = fst (compute_arguments_scope_full t)
 
+let check_arguments_scope_size ref scl =
+  let ty = Global.type_of_global ref in
+  let n = List.length scl in
+  try ignore (splay_prod_n (Global.env()) Evd.empty n ty)
+  with Invalid_argument _ ->
+    let n' = List.length (fst (splay_prod (Global.env()) Evd.empty ty)) in
+    errorlabstrm ""
+      (str "Found scopes for " ++ int n ++ str (plural n " argument") ++
+       str " while at most " ++ int n' ++
+       str (if n' = 1 then " was" else " were") ++ str " expected.")
+
 (** When merging scope list, we give priority to the first one (computed
     by substitution), using the second one (user given or earlier automatic)
     as fallback *)
@@ -543,6 +555,7 @@ let declare_arguments_scope_gen req r (scl,cls) =
 let declare_arguments_scope local ref scl =
   let req =
     if is_local local ref then ArgsScopeNoDischarge else ArgsScopeManual in
+  check_arguments_scope_size ref scl;
   declare_arguments_scope_gen req ref (scl,[])
 
 let find_arguments_scope r =
diff --git a/test-suite/bugs/closed/shouldsucceed/2667.v b/test-suite/bugs/closed/shouldsucceed/2667.v
new file mode 100644
index 0000000000..d920804d2d
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2667.v
@@ -0,0 +1,5 @@
+(* Check that not too many arguments are given to Arguments Scope *)
+
+Inductive stmt : Type := Sskip: stmt | Scall : nat -> stmt.
+Bind Scope Cminor with stmt.
+Fail Arguments Scope Scall [_ Cminor ]. (* At most 1 argument expected *)