From 94e0cbc26718fe3fecc58f6f8673f5f8abb0ce31 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 21 Jun 2017 15:12:21 +0200
Subject: [vernac] Remove stale bool parameter from `VernacStartTheoremProof`

`VernacStartTheoremProof` contained a stale bool parameter from 15
years ago, which is unused today.
---
 printing/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 4a5cfe6301..d0536a1744 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -698,7 +698,7 @@ open Decl_kinds
               | Some cc -> str" :=" ++ spc() ++ cc))
         )
 
-      | VernacStartTheoremProof (ki,l,_) ->
+      | VernacStartTheoremProof (ki,l) ->
         return (
           hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
                    prlist (pr_statement (spc () ++ keyword "with")) (List.tl l))
-- 
cgit v1.2.3