Addition of more general tactics for equality. Functional extensionality and eta expansion axioms for

dependent functions. Cleanup in Utils.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10260 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 5 deletions

diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index a87eda0a2..a268f0afb 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -28,8 +28,16 @@ Notation " ! " := (False_rect _ _).
 
 (** Abbreviation for first projection and hiding of proofs of subset objects. *)
 
+(** The scope in which programs are typed (not their types). *)
+
+Delimit Scope program_scope with prg.
+
 Notation " ` t " := (proj1_sig t) (at level 10) : core_scope.
-Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
+
+Delimit Scope subset_scope with subset.
+
+(* In [subset_scope] to allow masking by redefinitions for particular types. *)
+Notation "( x & ? )" := (@exist _ _ x _) : subset_scope.
 
 (** Coerces objects to their support before comparing them. *)
 
@@ -64,7 +72,3 @@ Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
 (* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *)
 (* Extract Inductive sigT => "prod" [ "" ]. *)
-
-(** The scope in which programs are typed (not their types). *)
-
-Delimit Scope program_scope with prg.