From a6f1944809e4caa6c99deb8c508dab9ad0e0071e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 10 Dec 2015 16:02:15 +0100
Subject: Silently ignore requests to _not_ clear something when that something
 cannot be cleared.

This should fix the contrib failures on tactics like "destruct (0)".
---
 tactics/tactics.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ce8b9b3dbd..536a10eaa7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -277,7 +277,8 @@ let apply_clear_request clear_flag dft c =
       error "keep/clear modifiers apply only to hypothesis names." in
   let clear = match clear_flag with
     | None -> dft && isVar c
-    | Some clear -> check_isvar c; clear in
+    | Some true -> check_isvar c; true
+    | Some false -> false in
   if clear then Proofview.V82.tactic (thin [destVar c])
   else Tacticals.New.tclIDTAC
 
-- 
cgit v1.2.3