aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/SetoidTactics.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Classes/SetoidTactics.v')
-rw-r--r--theories/Classes/SetoidTactics.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index fa939e22e..415c036a1 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -12,6 +12,7 @@
Institution: LRI, CNRS UMR 8623 - University Paris Sud
*)
+Require Coq.Classes.CRelationClasses Coq.Classes.CMorphisms.
Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions.
Require Import Coq.Classes.Equivalence Coq.Program.Basics.