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.

2 files changed, 3 insertions, 3 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
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index ddf78b1d4..b17330f13 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -34,7 +34,7 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
 
 (** {6 Primitive tactics. } *)
 
-val introduction    : ?check:bool -> Id.t -> unit Proofview.tactic
+val introduction    : Id.t -> unit Proofview.tactic
 val convert_concl   : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
 val convert_hyp     : ?check:bool -> named_declaration -> unit Proofview.tactic
 val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic