From e6edb3319c850cc7e30e5c31b0bfbf16c5c1a32c Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 7 Nov 2016 08:41:21 +0100 Subject: More explicit name for status of unification constraints. --- theories/Compat/Coq85.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Compat') diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index ba58e2d88..c64413383 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -29,4 +29,4 @@ 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 +Global Unset Solve Unification Constraints. -- cgit v1.2.3