diff options
| author | Pierre-Marie Pédrot | 2019-05-01 17:00:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-10 12:53:09 +0200 |
| commit | f7c55014aabb0d607449868e2522515db0b40568 (patch) | |
| tree | 16fc97ca5dcc475115b059a40425f10f0f53c5fa /tactics/tactics.mli | |
| parent | a5a89e8b623cd5822f59b854a45efc8236ae0087 (diff) | |
Make the check flag of conversion functions mandatory.
The current situation is a mess, some functions set it by default, but other
no. Making it mandatory ensures that the expected value is the correct one.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b3914816ac..3bb9a34509 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -33,8 +33,8 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) 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_concl : check:bool -> types -> cast_kind -> unit Proofview.tactic +val convert_hyp : check: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,13 +152,13 @@ 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_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 -val change_in_concl : ?check:bool -> (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic +val reduct_in_hyp : check: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 +val change_in_concl : check:bool -> (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic val change_concl : constr -> unit Proofview.tactic -val change_in_hyp : ?check:bool -> (occurrences * constr_pattern) option -> change_arg -> +val change_in_hyp : check:bool -> (occurrences * constr_pattern) option -> change_arg -> hyp_location -> unit Proofview.tactic val red_in_concl : unit Proofview.tactic val red_in_hyp : hyp_location -> unit Proofview.tactic @@ -180,7 +180,7 @@ val unfold_in_hyp : val unfold_option : (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic val change : - ?check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic + check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic val pattern_option : (occurrences * constr) list -> goal_location -> unit Proofview.tactic val reduce : red_expr -> clause -> unit Proofview.tactic |