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.
---
 interp/notation.mli | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index 38bd5fc7b8..85c4be4cc1 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -153,7 +153,9 @@ val find_arguments_scope : global_reference -> scope_name option list
 
 type scope_class
 
-val scope_class_of_reference : global_reference -> scope_class
+(** Comparison of scope_class *)
+val scope_class_compare : scope_class -> scope_class -> int
+
 val subst_scope_class :
   Mod_subst.substitution -> scope_class -> scope_class option
 
@@ -162,7 +164,8 @@ val declare_ref_arguments_scope : global_reference -> unit
 
 val compute_arguments_scope : Term.types -> scope_name option list
 val compute_type_scope : Term.types -> scope_name option
-val compute_scope_of_global : global_reference -> scope_name option
+
+val scope_class_of_class : Classops.cl_typ -> scope_class
 
 (** Building notation key *)
 
-- 
cgit v1.2.3


From 6aa58955515dff338ea85d59073dfc0d0c7648ab Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 24 Jun 2015 15:41:11 +0200
Subject: Move type_scope into user space, fix some output logs

---
 interp/notation.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index 85c4be4cc1..2bfbb33c2d 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -29,7 +29,6 @@ type scopes (** = [scope_name list] *)
 
 type local_scopes = tmp_scope_name option * scope_name list
 
-val type_scope : scope_name
 val declare_scope : scope_name -> unit
 
 val current_scopes : unit -> scopes
@@ -165,6 +164,9 @@ val declare_ref_arguments_scope : global_reference -> unit
 val compute_arguments_scope : Term.types -> scope_name option list
 val compute_type_scope : Term.types -> scope_name option
 
+(** Get the current scope bound to Sortclass, if it exists *)
+val current_type_scope_name : unit -> scope_name option
+
 val scope_class_of_class : Classops.cl_typ -> scope_class
 
 (** Building notation key *)
-- 
cgit v1.2.3