diff options
| author | Hugo Herbelin | 2019-04-28 16:29:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-04-29 21:20:28 +0200 |
| commit | b913a79738fee897bc298e0804617da8abcb4cf5 (patch) | |
| tree | 4e1315cb920f6600eb8aec728ba9812fc52a6e73 /plugins/ltac/tacexpr.ml | |
| parent | fcba5e87be13bc5a5374fe274476cd4d5c45f058 (diff) | |
Exposing a change_no_check tactic.
Diffstat (limited to 'plugins/ltac/tacexpr.ml')
| -rw-r--r-- | plugins/ltac/tacexpr.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 30e316b36d..0eb7726a18 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -34,6 +34,7 @@ type rec_flag = bool (* true = recursive false = not recursive *) type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) +type check_flag = bool (* true = check false = do not check *) type ('c,'d,'id) inversion_strength = | NonDepInversion of @@ -125,7 +126,7 @@ type 'a gen_atomic_tactic_expr = (* Conversion *) | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr - | TacChange of 'pat option * 'dtrm * 'nam clause_expr + | TacChange of check_flag * 'pat option * 'dtrm * 'nam clause_expr (* Equality and inversion *) | TacRewrite of evars_flag * |