From b02da518c51456b003c61f9775050fbfe6090629 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 25 Oct 2009 07:36:43 +0000
Subject: Improved the treatment of Local/Global options (noneffective Local on
 Implicit Arguments, Arguments Scope and Coercion fixed, noneffective Global
 in sections for Hints and Notation detected).

Misc. improvements (comments + interpretation of Hint Constructors +
dev printer for hint_db).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/notation.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 8f9f0959d5..e3eb38af60 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -475,6 +475,9 @@ let discharge_arguments_scope (_,(req,r,l)) =
   if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None
   else Some (req,Lib.discharge_global r,l)
 
+let classify_arguments_scope (req,_,_ as obj) =
+  if req = ArgsScopeNoDischarge then Dispose else Substitute obj
+
 let rebuild_arguments_scope (req,r,l) =
   match req with
     | ArgsScopeNoDischarge -> assert false
@@ -492,7 +495,7 @@ let (inArgumentsScope,outArgumentsScope) =
       cache_function = cache_arguments_scope;
       load_function = load_arguments_scope;
       subst_function = subst_arguments_scope;
-      classify_function = (fun o -> Substitute o);
+      classify_function = classify_arguments_scope;
       discharge_function = discharge_arguments_scope;
       rebuild_function = rebuild_arguments_scope }
 
-- 
cgit v1.2.3