From 0ad26633a4589d77de1f864733d1d953dab9ea91 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 19 Nov 2017 22:53:28 +0100 Subject: Fix (partial) #4878: option to stop autodeclaring axiom as instance. --- theories/Compat/Coq87.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'theories') 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. -- cgit v1.2.3