Essai de changement de sémantique du %scope :

1- ne s'applique plus que sur la notation immédiate au lieu de s'appliquer
   récursivement pour toutes les notations de l'expression concernée;
2- désactive la pile de scope pour cette notation immédiate.
Le point 2 est clairement préférable pour les notations de la forme
3%sc, où on ne veut pas que 3 soit interprété dans un autre scope
que sc même si sc n'a pas de notations numériques. Le point 1 est plus
discutable et risque aussi de poser des incompatibilité (mais le
comportement récursif peut être rétabli en changeant la valeur de
quelques booléens marqués "recursive" dans constrextern.ml,
constrintern.ml, et notation.ml).


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

1 files changed, 9 insertions, 6 deletions

diff --git a/interp/notation.mli b/interp/notation.mli
index d4c36d9e7..9822905c2 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -32,12 +32,15 @@ type delimiters = string
 type scope
 type scopes (* = [scope_name list] *)
 
+type local_scopes = tmp_scope_name option * scope_name list
+
 val type_scope : scope_name
 val declare_scope : scope_name -> unit
 
+val current_scopes : unit -> scopes
+
 (* Open scope *)
 
-val current_scopes : unit -> scopes
 val open_close_scope : 
   (* locality *) bool * (* open *) bool * scope_name -> unit
 
@@ -76,10 +79,10 @@ val declare_string_interpreter : scope_name -> required_module ->
 (* Return the [term]/[cases_pattern] bound to a primitive token in a
    given scope context*)
 
-val interp_prim_token : loc -> prim_token -> scope_name list -> 
+val interp_prim_token : loc -> prim_token -> local_scopes ->
   rawconstr * (notation_location * scope_name option)
 val interp_prim_token_cases_pattern : loc -> prim_token -> name -> 
-  scope_name list -> cases_pattern * (notation_location * scope_name option)
+  local_scopes -> cases_pattern * (notation_location * scope_name option)
 
 (* Return the primitive token associated to a [term]/[cases_pattern];
    raise [No_match] if no such token *)
@@ -90,7 +93,7 @@ val uninterp_prim_token_cases_pattern :
   cases_pattern -> name * scope_name * prim_token
 
 val availability_of_prim_token : 
-  scope_name -> scopes -> delimiters option option
+  scope_name -> local_scopes -> delimiters option option
 
 (*s Declare and interpret back and forth a notation *)
 
@@ -105,7 +108,7 @@ val declare_notation_interpretation : notation -> scope_name option ->
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
 (* Return the interpretation bound to a notation *)
-val interp_notation : loc -> notation -> scope_name list -> 
+val interp_notation : loc -> notation -> local_scopes ->
       interpretation * (notation_location * scope_name option)
 
 (* Return the possible notations for a given term *)
@@ -117,7 +120,7 @@ val uninterp_cases_pattern_notations : cases_pattern ->
 (* Test if a notation is available in the scopes *)
 (* context [scopes]; if available, the result is not None; the first *)
 (* argument is itself not None if a delimiters is needed *)
-val availability_of_notation : scope_name option * notation -> scopes -> 
+val availability_of_notation : scope_name option * notation -> local_scopes -> 
   (scope_name option * delimiters option) option
 
 (*s Declare and test the level of a (possibly uninterpreted) notation *)