diff options
| author | Hugo Herbelin | 2015-12-02 15:18:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-02 18:34:11 +0100 |
| commit | cc153dbbe45d5cf7f6ebfef6010adcc4f5bb568c (patch) | |
| tree | 228322f5b8b359db476f9a0428da61d68c29a589 /printing/pptactic.ml | |
| parent | 7a33a6284ba4e0953f82cf436fe324cdb95497e7 (diff) | |
Dead code from August 2014 in apply in.
Diffstat (limited to 'printing/pptactic.ml')
| -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 a669aef9a8..bc559460e0 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 } |