diff options
| author | Pierre-Marie Pédrot | 2014-08-06 01:10:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-06 02:10:38 +0200 |
| commit | b600c51753c5b60e62bdfcf1e6409afa1ce69d7a (patch) | |
| tree | 025367115bb871a5c04b3317125b3677e003cf22 /printing/pptactic.ml | |
| parent | dd37aea05fd568c98eb4d3970183c3dce1c23712 (diff) | |
Removing "intros untils" from the AST.
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 4c6afba114..1535bab9a7 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) -> |