diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 4c6afba11..1535bab9a 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -665,8 +665,6 @@ and pr_atom1 = function | TacIntroPattern (_::_ as p) -> hov 1 (str "intros" ++ spc () ++ prlist_with_sep spc Miscprint.pr_intro_pattern p) - | TacIntrosUntil h -> - hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h) | TacIntroMove (None,MoveLast) as t -> pr_atom0 t | TacIntroMove (Some id,MoveLast) -> str "intro " ++ pr_id id | TacIntroMove (ido,hto) -> |