Hide fast_done tactic

Author: ndcroos

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.