Silently ignore requests to _not_ clear something when that something cannot be cleared.

This should fix the contrib failures on tactics like "destruct (0)".

1 files changed, 2 insertions, 1 deletions

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