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

1 files changed, 0 insertions, 13 deletions

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 =