aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/Morphisms_Prop.v
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-15 18:23:31 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-15 18:23:31 +0000
commit4f2d820de5586a657d11e61377c3bdb82fcd5eeb (patch)
tree6c7622144abbbc871ecc5970c66f26e613df65aa /theories/Classes/Morphisms_Prop.v
parenta3645985be17e9fa8a8a5c4221aea40e189682c2 (diff)
Stop using [obligation_tactic] from Program.Tactics as the default
obligation tactic so that [Program] can work without importing anything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12330 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/Morphisms_Prop.v')
-rw-r--r--theories/Classes/Morphisms_Prop.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 1373e1952..b672651b9 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -16,6 +16,8 @@ Require Import Coq.Classes.Morphisms.
Require Import Coq.Program.Basics.
Require Import Coq.Program.Tactics.
+Obligation Tactic := simpl_relation.
+
(** Standard instances for [not], [iff] and [impl]. *)
(** Logical negation. *)