Removing Convert_concl and Convert_hyp from Logic.

6 files changed, 0 insertions, 40 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index ccb22f4a8..0e082077f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -687,16 +687,6 @@ let pr_prim_rule = function
       str(if Termops.occur_meta c then "refine " else "exact ") ++
       Constrextern.with_meta_as_hole pr_constr c
 
-  | Convert_concl (c,_) ->
-      (str"change "  ++ pr_constr c)
-
-  | Convert_hyp (id,None,t) ->
-      (str"change "  ++ pr_constr t  ++ spc ()  ++ str"in "  ++ pr_id id)
-
-  | Convert_hyp (id,Some c,t) ->
-      (str"change "  ++ pr_constr c  ++ spc ()  ++ str"in "
-       ++ pr_id id ++ str" (type of "  ++ pr_id id ++ str ")")
-
   | Thin ids ->
       (str"clear "  ++ pr_sequence pr_id ids)
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2d302510e..3be202476 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -655,20 +655,6 @@ let prim_refiner r sigma goal =
 	let sigma = Goal.V82.partial_solution sigma goal oterm in
 	  (sgl, sigma)
 
-    (* Conversion rules *)
-    | Convert_concl (cl',k) ->
-	check_typability env sigma cl';
-        let (sg,ev,sigma) = mk_goal sign cl' in
-	let sigma = check_conv_leq_goal env sigma cl' cl' cl in
-	let ev = if k != DEFAULTcast then mkCast(ev,k,cl) else ev in
-	let sigma = Goal.V82.partial_solution_to sigma goal sg ev in
-          ([sg], sigma)
-
-    | Convert_hyp (id,copt,ty) ->
-	let (gl,ev,sigma) = mk_goal (convert_hyp !check sign sigma (id,copt,ty)) cl in
-	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
-	([gl], sigma)
-
     (* And now the structural rules *)
     | Thin ids ->
         let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 2f0b0e608..925aff10e 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -32,8 +32,6 @@ type prim_rule =
   | FixRule of Id.t * int * (Id.t * int * constr) list * int
   | Cofix of Id.t * (Id.t * constr) list * int
   | Refine of constr
-  | Convert_concl of types * cast_kind
-  | Convert_hyp of named_declaration
   | Thin of Id.t list
   | Move of bool * Id.t * Id.t move_location
   | Rename of Id.t * Id.t
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 5fcdddeac..1fb73b7ad 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -24,8 +24,6 @@ type prim_rule =
   | FixRule of Id.t * int * (Id.t * int * constr) list * int
   | Cofix of Id.t * (Id.t * constr) list * int
   | Refine of constr
-  | Convert_concl of types * cast_kind
-  | Convert_hyp of named_declaration
   | Thin of Id.t list
   | Move of bool * Id.t * Id.t move_location
   | Rename of Id.t * Id.t
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 6c72009d4..c6f09eb2d 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -117,12 +117,6 @@ let internal_cut_rev_no_check replace id t gl =
 let refine_no_check c gl =
   refiner (Refine c) gl
 
-let convert_concl_no_check c sty gl =
-  refiner (Convert_concl (c,sty)) gl
-
-let convert_hyp_no_check d gl =
-  refiner (Convert_hyp d) gl
-
 (* This does not check dependencies *)
 let thin_no_check ids gl =
   if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl
@@ -148,8 +142,6 @@ let introduction id    = with_check (introduction_no_check id)
 let internal_cut b d t = with_check (internal_cut_no_check b d t)
 let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
 let refine c           = with_check (refine_no_check c)
-let convert_concl d sty = with_check (convert_concl_no_check d sty)
-let convert_hyp d      = with_check (convert_hyp_no_check d)
 let thin c             = with_check (thin_no_check c)
 let move_hyp b id id'  = with_check (move_hyp_no_check b id id')
 let rename_hyp l       = with_check (rename_hyp_no_check l)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index cebe78ed0..b754f6f40 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -84,8 +84,6 @@ val refiner                   : rule -> tactic
 val introduction_no_check     : Id.t -> tactic
 val internal_cut_no_check     : bool -> Id.t -> types -> tactic
 val refine_no_check           : constr -> tactic
-val convert_concl_no_check    : types -> cast_kind -> tactic
-val convert_hyp_no_check      : named_declaration -> tactic
 val thin_no_check             : Id.t list -> tactic
 val mutual_fix      :
   Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
@@ -97,8 +95,6 @@ val introduction     : Id.t -> tactic
 val internal_cut     : bool -> Id.t -> types -> tactic
 val internal_cut_rev : bool -> Id.t -> types -> tactic
 val refine           : constr -> tactic
-val convert_concl    : types -> cast_kind -> tactic
-val convert_hyp      : named_declaration -> tactic
 val thin             : Id.t list -> tactic
 val move_hyp         : bool -> Id.t -> Id.t move_location -> tactic
 val rename_hyp       : (Id.t*Id.t) list -> tactic