Hide fast_done tactic

coq-community · Jul 30, 2024 · cd217a1 · cd217a1
1 parent b4d9a0e
commit cd217a1
Showing 1 changed file with 24 additions and 15 deletions.
diff --git a/stdpp/stdpp_tactics.v b/stdpp/stdpp_tactics.v
@@ -2,6 +2,8 @@ Require Import
   MathClasses.misc.util.
 From Coq Require Export RelationClasses Relation_Definitions Lia.
 
+Module FastDoneTactic.
+
 Ltac fast_done :=
   solve
     [ eassumption
@@ -11,18 +13,25 @@ Ltac fast_done :=
 Tactic Notation "fast_by" tactic(tac) :=
   tac; fast_done.
 
-Ltac done :=
-  solve
-  [ repeat first
-    [ fast_done
-    | solve [trivial]
-    (* All the tactics below will introduce themselves anyway, or make no sense
-       for goals of product type. So this is a good place for us to do it. *)
-    | progress intros
-    | solve [symmetry; trivial]
-    | solve [apply not_symmetry; trivial]
-    | discriminate
-    | contradiction
-    | split
-    | match goal with H : ~ _ |- _ => case H; clear H; fast_done end ]
-  ].
+End FastDoneTactic.
+
+Section DoneSection.
+  Import FastDoneTactic.
+
+  Ltac done :=
+    solve
+    [ repeat first
+      [ fast_done
+      | solve [trivial]
+      (* All the tactics below will introduce themselves anyway, or make no sense
+         for goals of product type. So this is a good place for us to do it. *)
+      | progress intros
+      | solve [symmetry; trivial]
+      | solve [apply not_symmetry; trivial]
+      | discriminate
+      | contradiction
+      | split
+      | match goal with H : ~ _ |- _ => case H; clear H; fast_done end ]
+    ].
+
+End DoneSection.