diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 80711cf81..60bc784f1 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -456,7 +456,6 @@ let rec intern_atomic lf ist x = (* Basic tactics *) | TacIntroPattern l -> TacIntroPattern (List.map (intern_intro_pattern lf ist) l) - | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp) | TacIntroMove (ido,hto) -> TacIntroMove (Option.map (intern_ident lf ist) ido, intern_move_location ist hto) |