Tactics.introduction: remove dangerous option ~check

In locally nameless mode (proof mode) names in the context *must*
be distinct otherwise the term representation makes no sense.

1 files changed, 2 insertions, 2 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a42e4b44b..bb57e2bf4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -128,14 +128,14 @@ let unsafe_intro env store decl b =
     (sigma, mkNamedLambda_or_LetIn decl ev)
   end
 
-let introduction ?(check=true) id =
+let introduction id =
   Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     let hyps = named_context_val (Proofview.Goal.env gl) in
     let store = Proofview.Goal.extra gl in
     let env = Proofview.Goal.env gl in
-    let () = if check && mem_named_context_val id hyps then
+    let () = if mem_named_context_val id hyps then
       user_err ~hdr:"Tactics.introduction"
         (str "Variable " ++ Id.print id ++ str " is already declared.")
     in