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.
---
 test-suite/output/Cases.out      | 4 +++-
 test-suite/output/InitSyntax.out | 3 ++-
 test-suite/output/PrintInfos.out | 4 ++--
 3 files changed, 7 insertions(+), 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 09f032d478..92e70cf1cb 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,6 +6,8 @@ fix F (t : t) : P t :=
   end
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
+
+Argument scopes are [function_scope function_scope _]
      = fun d : TT => match d with
                      | @CTT _ _ b => b
                      end
@@ -24,7 +26,7 @@ match Nat.eq_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
-Argument scopes are [nat_scope nat_scope _ _ _]
+Argument scopes are [nat_scope nat_scope function_scope _ _]
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
   match l with
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index bbfd3405af..c17c63e724 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -4,7 +4,8 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
 For sig2: Argument A is implicit
 For exist2: Argument A is implicit
 For sig2: Argument scopes are [type_scope type_scope type_scope]
-For exist2: Argument scopes are [type_scope _ _ _ _ _]
+For exist2: Argument scopes are [type_scope function_scope function_scope _ _
+              _]
 exists x : nat, x = x
      : Prop
 fun b : bool => if b then b else b
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index ba076f050a..98420409e8 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -2,7 +2,7 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 existT is template universe polymorphic
 Argument A is implicit
-Argument scopes are [type_scope _ _ _]
+Argument scopes are [type_scope function_scope _ _]
 Expands to: Constructor Coq.Init.Specif.existT
 Inductive sigT (A : Type) (P : A -> Type) : Type :=
     existT : forall x : A, P x -> {x : A & P x}
@@ -10,7 +10,7 @@ Inductive sigT (A : Type) (P : A -> Type) : Type :=
 For sigT: Argument A is implicit
 For existT: Argument A is implicit
 For sigT: Argument scopes are [type_scope type_scope]
-For existT: Argument scopes are [type_scope _ _ _]
+For existT: Argument scopes are [type_scope function_scope _ _]
 existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 Argument A is implicit
-- 
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

---
 test-suite/bugs/closed/3080.v | 18 ++++++++++++++++++
 test-suite/bugs/closed/3612.v |  2 ++
 test-suite/bugs/closed/3649.v |  4 +++-
 3 files changed, 23 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/3080.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3080.v b/test-suite/bugs/closed/3080.v
new file mode 100644
index 0000000000..7d0dc090e1
--- /dev/null
+++ b/test-suite/bugs/closed/3080.v
@@ -0,0 +1,18 @@
+(* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
+Delimit Scope type_scope with type.
+Delimit Scope function_scope with function.
+
+Bind Scope type_scope with Sortclass.
+Bind Scope function_scope with Funclass.
+
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+
+Definition compose {A B C} (g : B -> C) (f : A -> B) :=
+  fun x : A => g (f x).
+
+Notation " g ∘ f " := (compose g f)
+  (at level 40, left associativity) : function_scope.
+
+Fail Check (fun x => x) ∘ (fun x => x). (* this [Check] should fail, as [function_scope] is not opened *)
+Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arugments to [compose] *)
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index 9125ab16dd..324c12525c 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -6,6 +6,8 @@ lines, then from 421 lines to 428 lines, then from 444 lines to 429 lines, then
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y  :>  T" (at level 70, y at next level, no associativity).
 Reserved Notation "x = y" (at level 70, no associativity).
+Delimit Scope type_scope with type.
+Bind Scope type_scope with Sortclass.
 Open Scope type_scope.
 Global Set Universe Polymorphism.
 Notation "A -> B" := (forall (_ : A), B) : type_scope.
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index 06188e7b1b..fc60897d21 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -4,6 +4,8 @@
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y" (at level 70, no associativity).
+Delimit Scope type_scope with type.
+Bind Scope type_scope with Sortclass.
 Open Scope type_scope.
 Axiom admit : forall {T}, T.
 Notation "A -> B" := (forall (_ : A), B) : type_scope.
@@ -54,4 +56,4 @@ Goal forall (C D : PreCategory) (G G' : Functor C D)
   (** This [change] succeeded, but did not progress, in 07e4438bd758c2ced8caf09a6961ccd77d84e42b, because [T0 x o T1 x] was not found in the goal *)
   let T0 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T0) end in
   let T1 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T1) end in
-  progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)).
\ No newline at end of file
+  progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)).
-- 
cgit v1.2.3