diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index a669aef9a..bc559460e 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -581,8 +581,7 @@ module Make let pr_in_hyp_as prc pr_id = function | None -> mt () - | Some (clear,id,ipat) -> - pr_in (spc () ++ pr_clear_flag clear pr_id id) ++ pr_as_ipat prc ipat + | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat let pr_clauses default_is_concl pr_id = function | { onhyps=Some []; concl_occs=occs } |