From 4a38c36307bf6333f6c26590820dfd82d643edf2 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 5 Apr 2008 21:32:11 +0000
Subject: Minor fixes: - Allow unicode superscripts characters. - Put Program
 notations in scopes. - Correct priority semantics in typeclasses eauto.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10759 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Subset.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'theories/Program/Subset.v')

diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index b6fc156c39..8ce84c8271 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -9,6 +9,8 @@
 Require Import Coq.Program.Utils.
 Require Import Coq.Program.Equality.
 
+Open Local Scope subset_scope.
+
 (** Tactics related to subsets and proof irrelevance. *)
 
 (** Simplify dependent equality using sigmas to equality of the codomains if possible. *)
@@ -72,7 +74,7 @@ Ltac clear_subset_proofs :=
 
 Ltac pi := repeat progress f_equal ; apply proof_irrelevance.
 
-Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> (`n) = (`m).
+Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> `n = `m.
 Proof.
   induction n.
   induction m.
-- 
cgit v1.2.3