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.

3 files changed, 7 insertions, 4 deletions

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