diff options
| author | Pierre-Marie Pédrot | 2015-12-03 15:08:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-03 15:13:02 +0100 |
| commit | 06a30c78c6148e8286c0904368bcc0f7c5af2c81 (patch) | |
| tree | 8581b27825cd3a6b5e1ced6061004f9b9ddd0f11 /printing | |
| parent | f5a752261f210e9c5ecbbbf54886904f0856975a (diff) | |
| parent | 6316e8b380a9942cd587f250eb4a69668e52019e (diff) | |
Merge branch 'v8.5'
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 72d2eedcc3..766222156a 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -586,8 +586,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 } |