From fb4ccbf4a7b66cc7af8b24e00fb19a0b49c769d1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 20 Jun 2016 20:21:27 +0200 Subject: Add Unset Shrink Abstract/Obligations in Coq85 For compatibility with 8.5. --- theories/Compat/Coq85.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'theories/Compat') diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index d6d370cb5..1e30ab919 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -15,3 +15,5 @@ Global Unset Bracketing Last Introduction Pattern. Global Unset Regular Subst Tactic. Global Unset Structural Injection. +Global Unset Shrink Abstract. +Global Unset Shrink Obligations. \ No newline at end of file -- cgit v1.2.3