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 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 38bd5fc7b..85c4be4cc 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