aboutsummaryrefslogtreecommitdiff
path: root/parsing/ppdecl_proof.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/ppdecl_proof.ml')
-rw-r--r--parsing/ppdecl_proof.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml
index ec8523d4d3..9e3de9838b 100644
--- a/parsing/ppdecl_proof.ml
+++ b/parsing/ppdecl_proof.ml
@@ -41,7 +41,6 @@ let pr_or_thesis pr_this env = function
Thesis Plain -> str "thesis"
| Thesis (For id) ->
str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id
- | Thesis (Sub n) -> str "thesis[" ++ int n ++ str "]"
| This c -> pr_this env c
let pr_cut pr_it env c =