From 30443ddaba7a0cc996216b3d692b97e0b05907fe Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 11 May 2008 22:04:26 +0000
Subject: - Cleanup parsing of binders, reducing to a single production for all
   binders. - Change syntax of type class instances to better match the usual
 syntax of   lemmas/definitions with name first, then arguments ":" instance. 
  Update theories/Classes accordingly. - Correct globalization of tactic
 references when doing Ltac :=/::=, update   documentation. - Remove the not
 so useful "(x &)" and "{{x}}" syntaxes from   Program.Utils, and subset_scope
 as well.

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

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

diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 8ce84c8271..c9de1a9e17 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -9,7 +9,7 @@
 Require Import Coq.Program.Utils.
 Require Import Coq.Program.Equality.
 
-Open Local Scope subset_scope.
+Open Local Scope program_scope.
 
 (** Tactics related to subsets and proof irrelevance. *)
 
-- 
cgit v1.2.3