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

2 files changed, 7 insertions, 16 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 =