Nouvelle approche pour le discharge modulaire

- Avant : une unique méthode discharge_function qui avait accès à l'ancien
  environnement mais pas de possibilité de raisonner avec les objets
  du nouvel environnement en cours de construction. C'était problématique
  pour le discharge des implicites, arguments scope, etc qui étaient
  finalement faits en même temps que le discharge des constantes et inductifs
  mais avec pour effets de bord que les entrées dans la lib_stk arrivaient 
  juste avant celles des constantes et inductifs avec des problèmes pour
  effacer les bonnes entrées au moment du reset
- Maintenant : deux méthodes distinctes : discharge_function qui est appliquée
  pour collecter de l'ancien environnement ce qui est à garder dans la
  section et rebuild_function qui reconstruit le nouvel environnement 
  connaissant déjà les nouvelles valeurs des objets précédants (on se rapproche
  ainsi plus de la méthode en deux temps d'avant la 8.1 tout en offrant
  l'extensibilité que la méthode ancienne du fichier discharge.ml ne
  permettait pas)

Au passage, ajout d'un modificateur Global aux déclarations
d'implicites et d'arguments scopes pour indiquer qu'elles doivent
perdurer à la sortie de la section
  
Au passage, suppression de l'objet DISCHARGED-HYPS-MAP et intégration
aux objets VARIABLE/CONSTANT/INDUCTIVE (seule la table des hyps
discharged reste)

Au passage, nettoyage impargs.ml, suppression code mort résiduel du
traducteur etc...



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

2 files changed, 20 insertions, 11 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 356c05e8f2..d08a9b06c0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -458,10 +458,14 @@ GEXTEND Gram
 	  VernacCoercion (Global, qid, s, t)
 
       (* Implicit *)
-      | IDENT "Implicit"; IDENT "Arguments"; qid = global; 
-         pos = OPT [ "["; l = LIST0 ident; "]" -> l ] ->
-	   let pos = option_map (List.map (fun id -> ExplByName id)) pos in
-	   VernacDeclareImplicits (qid,pos)
+      | IDENT "Implicit"; IDENT "Arguments"; 
+	 (local,qid,pos) = 
+	     [ local = [ IDENT "Global" -> false | IDENT "Local" -> true ];
+	       qid = global -> (local,qid,None) 
+	     | qid = global;
+	       l = OPT [ "["; l = LIST0 ident; "]" -> 
+		   List.map (fun id -> ExplByName id) l ] -> (true,qid,l) ] ->
+	   VernacDeclareImplicits (local,qid,pos)
 
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
 	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
@@ -712,8 +716,8 @@ GEXTEND Gram
      | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; 
        refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
 
-     | IDENT "Arguments"; IDENT "Scope"; qid = global;
-         "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
+     | IDENT "Arguments"; IDENT "Scope"; local = non_globality; qid = global;
+       "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (local,qid,scl)
 
      | IDENT "Infix"; local = locality;
 	 op = ne_string; ":="; p = global; 
@@ -746,6 +750,9 @@ GEXTEND Gram
   locality:
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
+  non_globality:
+    [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> true ] ]
+  ;
   level:
     [ [ IDENT "level"; n = natural -> NumLevel n
       | IDENT "next"; IDENT "level" -> NextLevel ] ]
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 6213e4fda7..e823a40d15 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -144,6 +144,7 @@ let pr_search a b pr_p = match a with
   | SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b
 
 let pr_locality local = if local then str "Local " else str ""
+let pr_non_globality local = if local then str "" else str "Global "
 
 let pr_explanation imps = function
   | ExplByPos n -> pr_id (Impargs.name_of_implicit (List.nth imps (n-1)))
@@ -447,10 +448,11 @@ let rec pr_vernac = function
   | VernacBindScope (sc,cll) ->
       str"Bind Scope" ++ spc () ++ str sc ++
       spc() ++ str "with " ++ prlist_with_sep spc pr_class_rawexpr cll
-  | VernacArgumentsScope (q,scl) -> let pr_opt_scope = function 
+  | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function 
       |	None -> str"_"
       |	Some sc -> str sc in 
-    str"Arguments Scope" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
+    str"Arguments Scope" ++ spc() ++ pr_non_globality local ++ pr_reference q 
+    ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
   | VernacInfix (local,(s,mv),q,sn) -> (* A Verifier *)
       hov 0 (hov 0 (str"Infix " ++ pr_locality local
       ++ qs s ++ str " :=" ++ spc() ++ pr_reference q) ++
@@ -746,11 +748,11 @@ let rec pr_vernac = function
         (str"Notation " ++ pr_locality local ++ pr_id id ++ str" :=" ++
          pr_constrarg c ++
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
-  | VernacDeclareImplicits (q,None) ->
+  | VernacDeclareImplicits (local,q,None) ->
       hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
-  | VernacDeclareImplicits (q,Some l) ->
+  | VernacDeclareImplicits (local,q,Some l) ->
       let r = Nametab.global q in
-      Impargs.declare_manual_implicits r l;
+      Impargs.declare_manual_implicits local r l;
       let imps = Impargs.implicits_of_global r in
       hov 1 (str"Implicit Arguments" ++ spc() ++ pr_reference q ++ spc() ++
              str"[" ++ prlist_with_sep sep (pr_explanation imps) l ++ str"]")