diff options
author | Jason Gross <jgross@mit.edu> | 2015-06-24 11:28:44 +0200 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2015-08-14 02:49:30 -0400 |
commit | 297b0cb44bbe8ec7304ca635c566815167266d4a (patch) | |
tree | b4efe113299e5832e68ae638a95847cdb2e92357 /test-suite/output/Cases.out | |
parent | 2bb05717bde540332aa814a59da3745f2097dedf (diff) |
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.
Diffstat (limited to 'test-suite/output/Cases.out')
-rw-r--r-- | test-suite/output/Cases.out | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 09f032d47..92e70cf1c 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 |