diff options
| author | Hugo Herbelin | 2019-04-29 21:01:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-04-29 21:01:49 +0200 |
| commit | fcba5e87be13bc5a5374fe274476cd4d5c45f058 (patch) | |
| tree | 14707fa1bd939458f553b1baaf35becda2267675 /tactics/tactics.mli | |
| parent | 69daead8ae18d55ee445a918865ea2adf59439eb (diff) | |
| parent | 7e8fbed8df5e3f819e4775df791fc85f235854fb (diff) | |
Merge PR #9983: Hypothesis conversion allocates a single evar
Reviewed-by: gares
Ack-by: herbelin
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 75b5caaa36..e7b95a820e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -36,7 +36,9 @@ 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_no_check : types -> cast_kind -> unit Proofview.tactic +[@@ocaml.deprecated "use [Tactics.convert_concl]"] val convert_hyp_no_check : named_declaration -> unit Proofview.tactic +[@@ocaml.deprecated "use [Tactics.convert_hyp]"] val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic val fix : Id.t -> int -> unit Proofview.tactic @@ -152,8 +154,8 @@ 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 : tactic_reduction * cast_kind -> unit Proofview.tactic -val e_reduct_in_concl : check:bool -> e_tactic_reduction * cast_kind -> 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 : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic val change_concl : constr -> unit Proofview.tactic val change_in_hyp : (occurrences * constr_pattern) option -> change_arg -> |