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.
---
 stm/stm.ml               | 2 +-
 stm/vernac_classifier.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 071d2edf98..81bac6a1f0 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -476,7 +476,7 @@ end = struct (* {{{ *)
   let mk_branch_name { expr = x } = Branch.make
     (let rec aux x = match x with
     | VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i
-    | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> Names.string_of_id i
+    | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.string_of_id i
     | VernacTime (_, e)
     | VernacTimeout (_, e) -> aux e
     | _ -> "branch" in aux x)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 1234e15afc..50e68852f8 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -115,7 +115,7 @@ let rec classify_vernac e =
         VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
     | VernacDefinition (_,((_,i),_),ProveBody _) ->
         VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater
-    | VernacStartTheoremProof (_,l,_) ->
+    | VernacStartTheoremProof (_,l) ->
         let ids = 
           CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
         VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
-- 
cgit v1.2.3