From 4fffbe45f42517fbe41fbcf4bf77bfa72fff2579 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 19 Jan 2021 10:34:22 -0800
Subject: Remove convert_concl_no_check

---
 tactics/tactics.ml  | 3 ---
 tactics/tactics.mli | 4 ----
 2 files changed, 7 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b40bdbc25e..3c51b0fe40 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -156,9 +156,6 @@ let convert_hyp ~check ~reorder d =
     end
   end
 
-let convert_concl_no_check = convert_concl ~check:false
-let convert_hyp_no_check = convert_hyp ~check:false ~reorder:false
-
 let convert_gen pb x y =
   Proofview.Goal.enter begin fun gl ->
     match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index a6471be549..d93f3bc434 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -35,10 +35,6 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
 val introduction    : Id.t -> unit Proofview.tactic
 val convert_concl   : check:bool -> types -> cast_kind -> unit Proofview.tactic
 val convert_hyp     : check:bool -> reorder:bool -> named_declaration -> unit Proofview.tactic
-val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
-[@@ocaml.deprecated "use [Tactics.convert_concl]"]
-val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
-[@@ocaml.deprecated "use [Tactics.convert_hyp]"]
 val mutual_fix      :
   Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic
 val fix             : Id.t -> int -> unit Proofview.tactic
-- 
cgit v1.2.3