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.
---
 intf/vernacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index b72577e1e0..94e3739d4a 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -292,7 +292,7 @@ type vernac_expr =
       obsolete_locality * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of obsolete_locality * (bool * scope_name)
   | VernacDelimiters of scope_name * string option
-  | VernacBindScope of scope_name * reference or_by_notation list
+  | VernacBindScope of scope_name * class_rawexpr list
   | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) *
       constr_expr * scope_name option
   | VernacNotation of
-- 
cgit v1.2.3