aboutsummaryrefslogtreecommitdiff
path: root/API
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-06-21 15:12:21 +0200
committerEmilio Jesus Gallego Arias2017-06-21 15:12:21 +0200
commit94e0cbc26718fe3fecc58f6f8673f5f8abb0ce31 (patch)
tree1a62e205de6964d9cff96ae0fe3a46319206e74a /API
parentd30ed5fe0694466f70eed51bc689cd0fa8c00da5 (diff)
[vernac] Remove stale bool parameter from `VernacStartTheoremProof`
`VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today.
Diffstat (limited to 'API')
-rw-r--r--API/API.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli
index 1e078bb77e..9f13f51fce 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2407,7 +2407,7 @@ sig
| VernacNotationAddFormat of string * string * string
| VernacDefinition of
(Decl_kinds.locality option * Decl_kinds.definition_object_kind) * plident * definition_expr
- | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list * bool
+ | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
| VernacEndProof of proof_end
| VernacExactProof of Constrexpr.constr_expr
| VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) *