diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-14 08:43:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-14 08:43:07 +0000 |
| commit | a89d858d0aea1a35d3e57d99ac0be7c6b494b282 (patch) | |
| tree | 07194dd29a52225fc5f262fe2ec34be060afc2cd /toplevel/vernacentries.ml | |
| 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/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b0f53b839..b3825dd93 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 |