diff options
| author | herbelin | 2002-10-14 08:43:07 +0000 |
|---|---|---|
| committer | herbelin | 2002-10-14 08:43:07 +0000 |
| commit | a89d858d0aea1a35d3e57d99ac0be7c6b494b282 (patch) | |
| tree | 07194dd29a52225fc5f262fe2ec34be060afc2cd /toplevel | |
| parent | e1240b1db05fc85083d9951edbe3ea3d8664404f (diff) | |
Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une
référence donnée
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3133 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 1 |
2 files changed, 5 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b0f53b8393..b3825dd932 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -289,6 +289,9 @@ let vernac_delimiters = Metasyntax.add_delimiters let vernac_open_scope = Symbols.open_scope +let vernac_arguments_scope qid scl = + Symbols.declare_arguments_scope (global qid) scl + let vernac_infix assoc n inf qid sc = let sp = sp_of_global None (global qid) in let dir = repr_dirpath (dirpath sp) in @@ -1032,6 +1035,7 @@ let interp c = match c with | VernacGrammar (univ,al) -> vernac_grammar univ al | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacOpenScope sc -> vernac_open_scope sc + | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl | VernacInfix (assoc,n,inf,qid,sc) -> vernac_infix assoc n inf qid sc | VernacDistfix (assoc,n,inf,qid,sc) -> vernac_distfix assoc n inf qid sc | VernacNotation (assoc,n,inf,c,sc) -> vernac_notation assoc n inf c sc diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index e0f0dc00e4..d2ad10bb6e 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -186,6 +186,7 @@ type vernac_expr = | VernacSyntax of string * syntax_entry_ast list | VernacOpenScope of scope_name | VernacDelimiters of scope_name * (string * string) + | VernacArgumentsScope of qualid located * scope_name option list | VernacInfix of grammar_associativity * int * string * qualid located * scope_name option | VernacDistfix of |