make pelim clearing optional

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Dec 29, 2023 · 933fe28 · 933fe28
1 parent 95a7794
commit 933fe28
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v
@@ -193,7 +193,7 @@ Ltac pelim q :=
   cbn;
   generalize dependent (q pt);
   nrapply paths_ind_r;
-  clear q.
+  try clear q.
 
 Tactic Notation "pelim" constr(x0) := pelim x0.
 Tactic Notation "pelim" constr(x0) constr(x1) := pelim x0; pelim x1.