From f629bd63917ca1fdacf5a3da4ee2ac7f3cba7398 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 4 Jan 2012 14:56:33 +0000
Subject: 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
---
 interp/notation.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'interp/notation.ml')

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 =
-- 
cgit v1.2.3