diff options
| author | Pierre-Marie Pédrot | 2019-05-01 17:22:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-10 12:53:09 +0200 |
| commit | d313bc5c1439f1881b4c77b9d92400579d2168ce (patch) | |
| tree | ce7a1a70d614a9e679a0002ce88d2cecb3d223aa /tactics/tactics.mli | |
| parent | f7c55014aabb0d607449868e2522515db0b40568 (diff) | |
Split the hypothesis conversion check in a conversion + ordering check.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 3bb9a34509..9eb8196280 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -34,7 +34,7 @@ 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 -> named_declaration -> 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 @@ -152,7 +152,7 @@ type e_tactic_reduction = Reductionops.e_reduction_function type change_arg = patvar_map -> env -> evar_map -> evar_map * constr val make_change_arg : constr -> change_arg -val reduct_in_hyp : check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic +val reduct_in_hyp : check:bool -> reorder:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic val reduct_option : check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic val reduct_in_concl : check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic val e_reduct_in_concl : check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic |