diff options
| -rw-r--r-- | printing/printer.ml | 10 | ||||
| -rw-r--r-- | proofs/logic.ml | 14 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 8 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 4 |
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 |