From c9f8f7fe182decedda2e6403d502fda3aff24a6e Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 22 Oct 2016 10:37:17 +0200 Subject: Add Unset Use Unif Heuristics in Compat/Coq85 --- theories/Compat/Coq85.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'theories/Compat') diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index 400753644..ba58e2d88 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -27,3 +27,6 @@ Global Set Refolding Reduction. Global Set Typeclasses Legacy Resolution. Global Set Typeclasses Limit Intros. Global Unset Typeclasses Filtered Unification. + +(** Allow silently letting unification constraints float after a "." *) +Global Unset Use Unification Heuristics. \ No newline at end of file -- cgit v1.2.3