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

10 files changed, 70 insertions, 194 deletions

diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 6ed79f23b7..7cf642ce7e 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -545,19 +545,21 @@ let ring_equality (r,add,mul,opp,req) =
                     error "ring opposite should be declared as a morphism" in
 		let op_morph =
 		  op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
-		  msgnl
+		  Flags.if_verbose 
+		    msgnl
 		    (str"Using setoid \""++pr_constr req++str"\""++spc()++  
-			str"and morphisms \""++pr_constr add_m ++
-			str"\","++spc()++ str"\""++pr_constr mul_m++
-			str"\""++spc()++str"and \""++pr_constr opp_m++
+			str"and morphisms \""++pr_constr add_m_lem ++
+			str"\","++spc()++ str"\""++pr_constr mul_m_lem++
+			str"\""++spc()++str"and \""++pr_constr opp_m_lem++
 			str"\"");
 		  op_morph)
             | None ->
-		(msgnl
+		(Flags.if_verbose
+		    msgnl
 		    (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++  
-			str"and morphisms \""++pr_constr add_m ++
+			str"and morphisms \""++pr_constr add_m_lem ++
 			str"\""++spc()++str"and \""++
-			pr_constr mul_m++str"\"");
+			pr_constr mul_m_lem++str"\"");
 		 op_smorph r add mul req add_m_lem mul_m_lem) in
           (setoid,op_morph)
 	    
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 2d1be640b1..e7a727bb5d 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -112,10 +112,7 @@ let vernac_assumption env isevars kind l nl =
 let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
-(*   check_required_library ["Coq";"Logic";"JMeq"]; *)
-  require_library "Coq.Program.Wf";
-  require_library "Coq.Program.Tactics";
-  require_library "Coq.Logic.JMeq";
+  check_required_library ["Coq";"Program";"Tactics"];
   let env = Global.env () in
   let isevars = ref (create_evar_defs Evd.empty) in
   try
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index e46ca822ee..54ed30a5dc 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1586,7 +1586,8 @@ let eq_id avoid id =
 
 let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
 let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y = mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
+let mk_JMeq typ x typ' y = 
+  mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
 let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |])
     
 let hole = RHole (dummy_loc, Evd.QuestionMark true)
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 9c40c861e1..a8bc546aae 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -176,6 +176,7 @@ let split_args n rel = match list_chop ((List.length rel) - n) rel with
   | _ -> assert(false)
 
 let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
+  Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let sigma = Evd.empty in
   let isevars = ref (Evd.create_evar_defs sigma) in
   let env = Global.env() in 
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index b684dd320b..dc79597dd4 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -64,9 +64,15 @@ let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
 let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
 let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro")
 
-let jmeq_ind = lazy (init_constant ["Logic";"JMeq"] "JMeq")
-let jmeq_rec = lazy (init_constant ["Logic";"JMeq"] "JMeq_rec")
-let jmeq_refl = lazy (init_constant ["Logic";"JMeq"] "JMeq_refl")
+let jmeq_ind =   
+  lazy (check_required_library ["Coq";"Logic";"JMeq"]; 
+	init_constant ["Logic";"JMeq"] "JMeq")
+let jmeq_rec = 
+  lazy (check_required_library ["Coq";"Logic";"JMeq"]; 
+	init_constant ["Logic";"JMeq"] "JMeq_rec")
+let jmeq_refl = 
+  lazy (check_required_library ["Coq";"Logic";"JMeq"];
+	init_constant ["Logic";"JMeq"] "JMeq_refl")
 
 let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
 let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 052d210196..b90fdc97e2 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -30,14 +30,21 @@ Definition equiv [ Equivalence A R ] : relation A := R.
 
 (** Shortcuts to make proof search possible (unification won't unfold equiv). *)
 
-Definition equivalence_refl [ sa : ! Equivalence A ] : Reflexive equiv.
-Proof. eauto with typeclass_instances. Qed.
+Program Instance [ sa : ! Equivalence A ] => equiv_refl : Reflexive equiv.
 
-Definition equivalence_sym [ sa : ! Equivalence A ] : Symmetric equiv.
-Proof. eauto with typeclass_instances. Qed.
+Program Instance [ sa : ! Equivalence A ] => equiv_sym : Symmetric equiv.
 
-Definition equivalence_trans [ sa : ! Equivalence A ] : Transitive equiv.
-Proof. eauto with typeclass_instances. Qed.
+  Next Obligation.
+  Proof.
+    symmetry ; auto.
+  Qed.
+
+Program Instance [ sa : ! Equivalence A ] => equiv_trans : Transitive equiv.
+
+  Next Obligation.
+  Proof.
+    transitivity y ; auto.
+  Qed.
 
 (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
 
@@ -70,16 +77,16 @@ Tactic Notation "clsubst" "*" := clsubst_nofail.
 Lemma nequiv_equiv_trans : forall [ ! Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
 Proof with auto.
   intros; intro.
-  assert(z === y) by relation_sym.
-  assert(x === y) by relation_trans.
+  assert(z === y) by (symmetry ; auto).
+  assert(x === y) by (transitivity z ; auto).
   contradiction.
 Qed.
 
 Lemma equiv_nequiv_trans : forall [ ! Equivalence A ] (x y z : A), x === y -> y =/= z -> x =/= z.
 Proof.
   intros; intro. 
-  assert(y === x) by relation_sym.
-  assert(y === z) by relation_trans.
+  assert(y === x) by (symmetry ; auto).
+  assert(y === z) by (transitivity x ; auto).
   contradiction.
 Qed.
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index dd964433c0..1eec3a24a9 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -71,16 +71,16 @@ Program Instance [ Equivalence A R, Equivalence B R' ] =>
   Next Obligation.
   Proof.
     constructor ; intros.
-    sym ; apply H.
-    sym ; auto.
+    symmetry ; apply H.
+    symmetry ; auto.
   Qed.
 
   Next Obligation.
   Proof.
     constructor ; intros.
-    trans (proj1_sig y y0).
+    transitivity (proj1_sig y y0).
     apply H ; auto.
-    apply H0. refl.
+    apply H0. reflexivity.
   Qed.
 
 (** Can't use the definition [notT] as it gives a universe inconsistency. *)
@@ -227,7 +227,7 @@ Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => reflexive_impl_
   
   Next Obligation.
   Proof.
-    split ; apply respect ; [ auto | sym ] ; auto.
+    split ; apply respect ; [ auto | symmetry ] ; auto.
   Qed.
 
 (** The complement of a relation conserves its morphisms. *)
@@ -314,8 +314,8 @@ Program Instance [ ! Transitive A (R : relation A) ] =>
 
   Next Obligation.
   Proof with auto.
-    trans x...
-    trans x0...
+    transitivity x...
+    transitivity x0...
   Qed.
 
 (** Dually... *)
@@ -351,7 +351,7 @@ Program Instance [ ! Transitive A R ] (x : A) =>
 
   Next Obligation.
   Proof with auto.
-    trans y...
+    transitivity y...
   Qed.
 
 Program Instance [ ! Transitive A R ] (x : A) =>
@@ -359,7 +359,7 @@ Program Instance [ ! Transitive A R ] (x : A) =>
 
   Next Obligation.
   Proof with auto.
-    trans x0...
+    transitivity x0...
   Qed.
 
 Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
@@ -367,8 +367,8 @@ Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
 
   Next Obligation.
   Proof with auto.
-    trans y...
-    sym...
+    transitivity y...
+    symmetry...
   Qed.
 
 Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
@@ -376,8 +376,8 @@ Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
 
   Next Obligation.
   Proof with auto.
-    trans x0...
-    sym...
+    transitivity x0...
+    symmetry...
   Qed.
 
 Program Instance [ Equivalence A R ] (x : A) =>
@@ -385,10 +385,10 @@ Program Instance [ Equivalence A R ] (x : A) =>
 
   Next Obligation.
   Proof with auto.
-    split. intros ; trans x0...
+    split. intros ; transitivity x0...
     intros.
-    trans y...
-    sym...
+    transitivity y...
+    symmetry...
   Qed.
 
 (** With symmetric relations, variance is no issue ! *)
@@ -413,7 +413,7 @@ Program Instance (A B : Type) (R : relation A) (R' : relation B)
   Proof with auto.
     intros.
     apply (respect (m:=m))...
-    refl.
+    reflexivity.
   Qed.
 
 (** Every transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
@@ -424,7 +424,7 @@ Program Instance [ ! Transitive A R ] =>
 
   Next Obligation.
   Proof with auto.
-    trans y...
+    transitivity y...
     subst x0...
   Qed.
 
@@ -433,7 +433,7 @@ Program Instance [ ! Transitive A R ] =>
 
   Next Obligation.
   Proof with auto.
-    trans x...
+    transitivity x...
     subst x0...
   Qed.
 
@@ -445,9 +445,9 @@ Program Instance [ ! Transitive A R, Symmetric R ] =>
   Next Obligation.
   Proof with auto.
     split ; intros.
-    trans x0... trans x... sym...
+    transitivity x0... transitivity x... symmetry...
   
-    trans y... trans y0... sym...
+    transitivity y... transitivity y0... symmetry...
   Qed.
 
 Program Instance [ Equivalence A R ] => 
@@ -456,9 +456,9 @@ Program Instance [ Equivalence A R ] =>
   Next Obligation.
   Proof with auto.
     split ; intros.
-    trans x0... trans x... sym...
+    transitivity x0... transitivity x... symmetry...
   
-    trans y... trans y0... sym...
+    transitivity y... transitivity y0... symmetry...
   Qed.
 
 (** In case the rewrite happens at top level. *)
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 659f9528cd..20ac475b9e 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -161,144 +161,6 @@ Program Instance eq_refl : Reflexive (@eq A).
 Program Instance eq_sym : Symmetric (@eq A).
 Program Instance eq_trans : Transitive (@eq A).
 
-(** ** General tactics to solve goals on relations.
-   Each tactic comes in two flavors:
-   - a tactic to immediately solve a goal without user intervention
-   - a tactic taking input from the user to make progress on a goal *)
-
-Definition relate A (R : relation A) : relation A := R.
-
-Ltac relationify_relation R R' :=
-  match goal with
-    | [ H : context [ R ?x ?y ] |- _ ] => change (R x y) with (R' x y) in H
-    | [ |- context [ R ?x ?y ] ] => change (R x y) with (R' x y)
-  end.
-
-Ltac relationify R :=
-  set (R' := relate R) ; progress (repeat (relationify_relation R R')).
-
-Ltac relation_refl :=
-  match goal with
-    | [ |- ?R ?X ?X ] => apply (reflexive (R:=R) X)
-    | [ H : ?R ?X ?X |- _ ] => apply (irreflexive (R:=R) H)
-
-    | [ |- ?R ?A ?X ?X ] => apply (reflexive (R:=R A) X)
-    | [ H : ?R ?A ?X ?X |- _ ] => apply (irreflexive (R:=R A) H)
-
-    | [ |- ?R ?A ?B ?X ?X ] => apply (reflexive (R:=R A B) X)
-    | [ H : ?R ?A ?B ?X ?X |- _ ] => apply (irreflexive (R:=R A B) H)
-
-    | [ |- ?R ?A ?B ?C ?X ?X ] => apply (reflexive (R:=R A B C) X)
-    | [ H : ?R ?A ?B ?C ?X ?X |- _ ] => apply (irreflexive (R:=R A B C) H)
-
-    | [ |- ?R ?A ?B ?C ?D ?X ?X ] => apply (reflexive (R:=R A B C D) X)
-    | [ H : ?R ?A ?B ?C ?D ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D) H)
-
-    | [ |- ?R ?A ?B ?C ?D ?E ?X ?X ] => apply (reflexive (R:=R A B C D E) X)
-    | [ H : ?R ?A ?B ?C ?D ?E ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E) H)
-
-    | [ |- ?R ?A ?B ?C ?D ?E ?F ?X ?X ] => apply (reflexive (R:=R A B C D E F) X)
-    | [ H : ?R ?A ?B ?C ?D ?E ?F ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E F) H)
-
-    | [ |- ?R ?A ?B ?C ?D ?E ?F ?G ?X ?X ] => apply (reflexive (R:=R A B C D E F G) X)
-    | [ H : ?R ?A ?B ?C ?D ?E ?F ?G ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E F G) H)
-
-    | [ |- ?R ?A ?B ?C ?D ?E ?F ?G ?H ?X ?X ] => apply (reflexive (R:=R A B C D E F G H) X)
-    | [ H : ?R ?A ?B ?C ?D ?E ?F ?G ?H ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E F G H) H)
-  end.
-
-Ltac refl := relation_refl.
-
-Ltac relation_sym := 
-  match goal with
-    | [ H : ?R ?X ?Y |- ?R ?Y ?X ] => apply (symmetric (R:=R) (x:=X) (y:=Y) H)
-
-    | [ H : ?R ?A ?X ?Y |- ?R ?A ?Y ?X ] => apply (symmetric (R:=R A) (x:=X) (y:=Y) H)
-
-    | [ H : ?R ?A ?B ?X ?Y |- ?R ?A ?B ?Y ?X ] => apply (symmetric (R:=R A B) (x:=X) (y:=Y) H)
-
-    | [ H : ?R ?A ?B ?C ?X ?Y |- ?R ?A ?B ?C ?Y ?X ] => apply (symmetric (R:=R A B C) (x:=X) (y:=Y) H)
-
-    | [ H : ?R ?A ?B ?C ?D ?X ?Y |- ?R ?A ?B ?C ?D ?Y ?X ] => apply (symmetric (R:=R A B C D) (x:=X) (y:=Y) H)
-
-    | [ H : ?R ?A ?B ?C ?D ?E ?X ?Y |- ?R ?A ?B ?C ?D ?E ?Y ?X ] => apply (symmetric (R:=R A B C D E) (x:=X) (y:=Y) H)
-
-    | [ H : ?R ?A ?B ?C ?D ?E ?F ?X ?Y |- ?R ?A ?B ?C ?D ?E ?F ?Y ?X ] => apply (symmetric (R:=R A B C D E F) (x:=X) (y:=Y) H)
-  end.
-
-Ltac relation_symmetric := 
-  match goal with
-    | [ |- ?R ?Y ?X ] => apply (symmetric (R:=R) (x:=X) (y:=Y))
-
-    | [ |- ?R ?A ?Y ?X ] => apply (symmetric (R:=R A) (x:=X) (y:=Y))
-
-    | [ |- ?R ?A ?B ?Y ?X ] => apply (symmetric (R:=R A B) (x:=X) (y:=Y))
-
-    | [ |- ?R ?A ?B ?C ?Y ?X ] => apply (symmetric (R:=R A B C) (x:=X) (y:=Y))
-
-    | [ |- ?R ?A ?B ?C ?D ?Y ?X ] => apply (symmetric (R:=R A B C D) (x:=X) (y:=Y))
-
-    | [ |- ?R ?A ?B ?C ?D ?E ?Y ?X ] => apply (symmetric (R:=R A B C D E) (x:=X) (y:=Y))
-
-    | [ |- ?R ?A ?B ?C ?D ?E ?F ?Y ?X ] => apply (symmetric (R:=R A B C D E F) (x:=X) (y:=Y))
-  end.
-
-Ltac sym := relation_symmetric.
-
-Ltac relation_trans := 
-  match goal with
-    | [ H : ?R ?X ?Y, H' : ?R ?Y ?Z |- ?R ?X ?Z ] => 
-      apply (transitive (R:=R) (x:=X) (y:=Y) (z:=Z) H H')
-
-    | [ H : ?R ?A ?X ?Y, H' : ?R ?A ?Y ?Z |- ?R ?A ?X ?Z ] => 
-      apply (transitive (R:=R A) (x:=X) (y:=Y) (z:=Z) H H')
-
-    | [ H : ?R ?A ?B ?X ?Y, H' : ?R ?A ?B ?Y ?Z |- ?R ?A ?B ?X ?Z ] => 
-      apply (transitive (R:=R A B) (x:=X) (y:=Y) (z:=Z) H H')
-
-    | [ H : ?R ?A ?B ?C ?X ?Y, H' : ?R ?A ?B ?C ?Y ?Z |- ?R ?A ?B ?C ?X ?Z ] => 
-      apply (transitive (R:=R A B C) (x:=X) (y:=Y) (z:=Z) H H')
-
-    | [ H : ?R ?A ?B ?C ?D ?X ?Y, H' : ?R ?A ?B ?C ?D ?Y ?Z |- ?R ?A ?B ?C ?D ?X ?Z ] => 
-      apply (transitive (R:=R A B C D) (x:=X) (y:=Y) (z:=Z) H H')
-
-    | [ H : ?R ?A ?B ?C ?D ?E ?X ?Y, H' : ?R ?A ?B ?C ?D ?E ?Y ?Z |- ?R ?A ?B ?C ?D ?E ?X ?Z ] => 
-      apply (transitive (R:=R A B C D E) (x:=X) (y:=Y) (z:=Z) H H')
-
-    | [ H : ?R ?A ?B ?C ?D ?E ?F ?X ?Y, H' : ?R ?A ?B ?C ?D ?E ?F ?Y ?Z |- ?R ?A ?B ?C ?D ?E ?F ?X ?Z ] => 
-      apply (transitive (R:=R A B C D E F) (x:=X) (y:=Y) (z:=Z) H H')
-  end.
-
-Ltac relation_transitive Y := 
-  match goal with
-    | [ |- ?R ?X ?Z ] => 
-      apply (transitive (R:=R) (x:=X) (y:=Y) (z:=Z))
-
-    | [ |- ?R ?A ?X ?Z ] => 
-      apply (transitive (R:=R A) (x:=X) (y:=Y) (z:=Z))
-
-    | [ |- ?R ?A ?B ?X ?Z ] => 
-      apply (transitive (R:=R A B) (x:=X) (y:=Y) (z:=Z))
-
-    | [ |- ?R ?A ?B ?C ?X ?Z ] => 
-      apply (transitive (R:=R A B C) (x:=X) (y:=Y) (z:=Z))
-
-    | [ |- ?R ?A ?B ?C ?D ?X ?Z ] => 
-      apply (transitive (R:=R A B C D) (x:=X) (y:=Y) (z:=Z))
-
-    | [ |- ?R ?A ?B ?C ?D ?E ?X ?Z ] => 
-      apply (transitive (R:=R A B C D E) (x:=X) (y:=Y) (z:=Z))
-
-    | [ |- ?R ?A ?B ?C ?D ?E ?F ?X ?Z ] => 
-      apply (transitive (R:=R A B C D E F) (x:=X) (y:=Y) (z:=Z))
-  end.
-
-Ltac trans Y := relation_transitive Y.
-
-(** To immediatly solve a goal on setoid equality. *)
-
-Ltac relation_tac := relation_refl || relation_sym || relation_trans.
-
 (** Various combinations of reflexivity, symmetry and transitivity. *)
 
 (** A [PreOrder] is both reflexive and transitive. *)
@@ -323,8 +185,9 @@ Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] =>
   Next Obligation.
   Proof with auto.
     constructor ; intros...
-    assert(R x0 x0) by (trans y0 ; [ auto | sym ; auto ]).
-    trans (y x0)...
+    assert(R x0 x0). 
+    clapply transitive. clapply symmetric.
+    clapply transitive. 
   Qed.
 
 (** The [Equivalence] typeclass. *)
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 4ae44b3b4e..b355c3c088 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -89,16 +89,16 @@ Tactic Notation "clsubst" "*" := clsubst_nofail.
 Lemma nequiv_equiv_trans : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z.
 Proof with auto.
   intros; intro.
-  assert(z == y) by relation_sym.
-  assert(x == y) by relation_trans.
+  assert(z == y) by (symmetry ; auto).
+  assert(x == y) by (transitivity z ; eauto).
   contradiction.
 Qed.
 
 Lemma equiv_nequiv_trans : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z.
 Proof.
   intros; intro. 
-  assert(y == x) by relation_sym.
-  assert(y == z) by relation_trans.
+  assert(y == x) by (symmetry ; auto).
+  assert(y == z) by (transitivity x ; eauto).
   contradiction.
 Qed.
 
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.
-