diff options
| author | Maxime Dénès | 2017-06-23 17:14:24 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-23 17:14:24 +0200 |
| commit | f258dd1954f4ab738a987798630cfaaddfb9de37 (patch) | |
| tree | 8f5d1f02f307156075c2f952aab1de3daf489cd7 /intf | |
| parent | 7cc335bd4cc568bdf892da60ebd16e6acfe019cd (diff) | |
| parent | 94e0cbc26718fe3fecc58f6f8673f5f8abb0ce31 (diff) | |
Merge PR#821: [vernac] Remove stale bool parameter from `VernacStartTheoremProof`
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 7c12f9df5d..31ec444707 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -331,7 +331,7 @@ type vernac_expr = (* Gallina *) | VernacDefinition of (locality option * definition_object_kind) * plident * definition_expr - | VernacStartTheoremProof of theorem_kind * proof_expr list * bool + | VernacStartTheoremProof of theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * |