aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Compat/Coq87.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Compat/Coq87.v')
-rw-r--r--theories/Compat/Coq87.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v
index ef1737bf8..aeef9595d 100644
--- a/theories/Compat/Coq87.v
+++ b/theories/Compat/Coq87.v
@@ -15,3 +15,6 @@
and breaks at least fiat-crypto. *)
Declare ML Module "omega_plugin".
Unset Omega UseLocalDefs.
+
+
+Set Typeclasses Axioms Are Instances.