diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-05 15:56:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-09 16:04:42 +0200 |
| commit | 68a7940b2d6b03fd511faf8ad8a65edc9f7aa0e1 (patch) | |
| tree | 281501dd118cd87dfc6d0b90d6062971920c5ad6 /proofs/tacmach.mli | |
| parent | e824d429363262a9ff9db117282fe15289b5ab59 (diff) | |
Removing Convert_concl and Convert_hyp from Logic.
Diffstat (limited to 'proofs/tacmach.mli')
| -rw-r--r-- | proofs/tacmach.mli | 4 |
1 files changed, 0 insertions, 4 deletions
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 |