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, 12 insertions, 9 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 44e7cbad78..4c24f35056 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -284,8 +284,8 @@ let vernac_bind_scope sc cll =
 
 let vernac_open_close_scope = Notation.open_close_scope
 
-let vernac_arguments_scope qid scl =
-  Notation.declare_arguments_scope (global qid) scl
+let vernac_arguments_scope local qid scl =
+  Notation.declare_arguments_scope local (global qid) scl
 
 let vernac_infix = Metasyntax.add_infix
 
@@ -666,9 +666,11 @@ let vernac_hints = Auto.add_hints
 
 let vernac_syntactic_definition = Command.syntax_definition 
 
-let vernac_declare_implicits locqid = function
-  | Some imps -> Impargs.declare_manual_implicits (Nametab.global locqid) imps
-  | None -> Impargs.declare_implicits (Nametab.global locqid)
+let vernac_declare_implicits local locqid = function
+  | Some imps ->
+      Impargs.declare_manual_implicits local (Nametab.global locqid) imps
+  | None -> 
+      Impargs.declare_implicits local (Nametab.global locqid)
 
 let vernac_reserve idl c =
   let t = Constrintern.interp_type Evd.empty (Global.env()) c in
@@ -1122,7 +1124,7 @@ let interp c = match c with
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
   | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
   | VernacOpenCloseScope sc -> vernac_open_close_scope sc
-  | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl
+  | VernacArgumentsScope (lcl,qid,scl) -> vernac_arguments_scope lcl qid scl
   | VernacInfix (local,mv,qid,sc) -> vernac_infix local mv qid sc
   | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc
 
@@ -1193,7 +1195,7 @@ let interp c = match c with
   | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
   | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
   | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
-  | VernacDeclareImplicits (qid,l) -> vernac_declare_implicits qid l
+  | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
   | VernacReserve (idl,c) -> vernac_reserve idl c
   | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl
   | VernacSetOption (key,v) -> vernac_set_option key v
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index ffde10192b..825e8d5494 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -180,7 +180,7 @@ type vernac_expr =
   | VernacOpenCloseScope of (locality_flag * bool * scope_name)
   | VernacDelimiters of scope_name * lstring
   | VernacBindScope of scope_name * class_rawexpr list
-  | VernacArgumentsScope of lreference * scope_name option list
+  | VernacArgumentsScope of locality_flag * lreference * scope_name option list
   | VernacInfix of locality_flag * (lstring * syntax_modifier list) *
       lreference * scope_name option
   | VernacNotation of
@@ -259,7 +259,8 @@ type vernac_expr =
   | VernacHints of locality_flag * lstring list * hints
   | VernacSyntacticDefinition of identifier * constr_expr * locality_flag *
       onlyparsing_flag
-  | VernacDeclareImplicits of lreference * explicitation list option
+  | VernacDeclareImplicits of locality_flag * lreference *
+      explicitation list option
   | VernacReserve of lident list * constr_expr
   | VernacSetOpacity of opacity_flag * lreference list
   | VernacUnsetOption of Goptions.option_name