Backtracking on r14876 (fix for bug #2267): extra scopes might be

useful in the presence of coercions to Funclass. Fixed the bug
differently.

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

4 files changed, 22 insertions, 18 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 656baa9465..3d39f0f928 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -731,9 +731,13 @@ let apply_scope_env env = function
   | [] -> {env with tmp_scope = None}, []
   | sc::scl -> {env with tmp_scope = sc}, scl
 
-let rec simple_adjust_scopes n = function
-  | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
-  | sc::scopes -> assert (n>0); sc :: simple_adjust_scopes (n-1) scopes
+let rec simple_adjust_scopes n scopes =
+  (* Note: they can be less scopes than arguments but also more scopes *)
+  (* than arguments because extra scopes are used in the presence of *)
+  (* coercions to funclass *)
+  if n=0 then [] else match scopes with
+  | [] -> None :: simple_adjust_scopes (n-1) []
+  | sc::scopes -> 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 9a88ad75d8..8f19ab851f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -18,7 +18,6 @@ open Summary
 open Glob_term
 open Topconstr
 open Ppextend
-open Reductionops
 (*i*)
 
 (*s A scope is a set of notations; it includes
@@ -470,17 +469,6 @@ 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 *)
@@ -555,7 +543,6 @@ 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
index d920804d2d..0631e5358d 100644
--- a/test-suite/bugs/closed/shouldsucceed/2667.v
+++ b/test-suite/bugs/closed/shouldsucceed/2667.v
@@ -1,5 +1,11 @@
-(* Check that not too many arguments are given to Arguments Scope *)
+(* Check that extra arguments to Arguments Scope do not disturb use of *)
+(* scopes in constructors *)
 
 Inductive stmt : Type := Sskip: stmt | Scall : nat -> stmt.
 Bind Scope Cminor with stmt.
-Fail Arguments Scope Scall [_ Cminor ]. (* At most 1 argument expected *)
+
+(* extra argument is ok because of possible coercion to funclass *)
+Arguments Scope Scall [_ Cminor ].
+
+(* extra argument is ok because of possible coercion to funclass *)
+Fixpoint f (c: stmt) : Prop := match c with Scall _ => False | _ => False end.
diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v
index 55d8343efa..5b37dbd4e1 100644
--- a/test-suite/success/Scopes.v
+++ b/test-suite/success/Scopes.v
@@ -6,3 +6,10 @@ Module A.
 Definition opp := Zopp.
 End A.
 Check (A.opp 3).
+
+(* Test extra scopes to be used in the presence of coercions *)
+
+Record B := { f :> Z -> Z }.
+Variable a:B.
+Arguments Scope a [Z_scope].
+Check a 0.