diff options
Diffstat (limited to 'ltac/tacintern.ml')
| -rw-r--r-- | ltac/tacintern.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index bd48ffb723..c1c7be1cc9 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -481,7 +481,6 @@ let rec intern_atomic lf ist x = (* Basic tactics *) | TacIntroPattern l -> TacIntroPattern (List.map (intern_intro_pattern lf ist) l) - | TacExact c -> TacExact (intern_constr ist c) | TacApply (a,ev,cb,inhyp) -> TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb, Option.map (intern_in_hyp_as ist lf) inhyp) |