From 9e1ab25ce311b5c0e18e1023eaaa38673a38d3d5 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 16 Mar 2008 17:48:43 +0000
Subject: Removed unneeded tactics from RelationClasses. Use
 check_required_library where needed (fixes bug #1797). Remove spurious
 messages from ring when not in verbose mode.

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

(limited to 'theories/Program')

diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index c414dc9cd6..b6fc156c39 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -88,7 +88,7 @@ Qed.
 (* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f] 
    in tactics. *)
 
-Program Definition match_eq (A B : Type) (x : A) (fn : forall (y : A | y = x), B) : B :=
+Definition match_eq (A B : Type) (x : A) (fn : forall (y : A | y = x), B) : B :=
   fn (exist _ x (refl_equal x)).
 
 (* This is what we want to be able to do: replace the originaly matched object by a new, 
@@ -122,4 +122,3 @@ Ltac rewrite_match_eq H :=
 (** Otherwise we can simply unfold [match_eq] and the term trivially reduces to the original definition. *)
 
 Ltac simpl_match_eq := unfold match_eq ; simpl.
-
-- 
cgit v1.2.3