From 297b0cb44bbe8ec7304ca635c566815167266d4a Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 24 Jun 2015 11:28:44 +0200
Subject: 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.
---
 stm/texmacspp.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'stm')

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 _
-- 
cgit v1.2.3