diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index b1d6fb0c0f..f4007e25e1 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -854,11 +854,6 @@ module Make pr_with_occurrences pr.pr_constr cl ++ pr_as_name na) l ) - | TacGeneralizeDep c -> - hov 1 ( - primitive "generalize" ++ spc () ++ str "dependent" - ++ pr_constrarg c - ) | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl -> hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c) | TacLetTac (na,c,cl,b,e) -> |