diff options
| author | Jason Gross | 2015-06-24 11:28:44 +0200 |
|---|---|---|
| committer | Jason Gross | 2015-08-14 02:49:30 -0400 |
| commit | 297b0cb44bbe8ec7304ca635c566815167266d4a (patch) | |
| tree | b4efe113299e5832e68ae638a95847cdb2e92357 /stm | |
| parent | 2bb05717bde540332aa814a59da3745f2097dedf (diff) | |
Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080
This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change
in the semantics of arguments scopes: scopes can no longer be bound to
Funclass or Sortclass (this does not seem to be useful)). It is
useful to have function_scope for, e.g., function composition. This
allows users to, e.g., automatically interpret ∘ as morphism
composition when expecting a morphism of categories, as functor
composition when expecting a functor, and as function composition when
expecting a function.
Additionally, it is nicer to have fewer special cases in the OCaml
code, and give more things a uniform syntax. (The scope type_scope
should not be special-cased; this change is coming up next.)
Also explicitly define [function_scope] in theories/Init/Notations.v.
This closes bug #3080, Build a [function_scope] like [type_scope], or allow
[Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass]
We now mention Funclass and Sortclass in the documentation of [Bind Scope]
again.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/texmacspp.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index aaa6c2c07d..af506015de 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -513,13 +513,6 @@ let rec tmpp v loc = xmlScope loc "delimit" name ~attr:["delimiter",tag] [] | VernacDelimiters (name,None) -> xmlScope loc "undelimit" name ~attr:[] [] - | VernacBindScope (name,l) -> - xmlScope loc "bind" name - (List.map (function - | ByNotation(loc,name,None) -> xmlNotation [] name loc [] - | ByNotation(loc,name,Some d) -> - xmlNotation ["delimiter",d] name loc [] - | AN ref -> xmlReference ref) l) | VernacInfix (_,((_,name),sml),ce,sn) -> let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in let sc_attr = @@ -535,6 +528,7 @@ let rec tmpp v loc = | Some scope -> ["scope", scope] | None -> [] in xmlNotation (sc_attr @ attrs) name loc [pp_expr ce] + | VernacBindScope _ as x -> xmlTODO loc x | VernacNotationAddFormat _ as x -> xmlTODO loc x | VernacUniverse _ | VernacConstraint _ |