aboutsummaryrefslogtreecommitdiff
path: root/coqpp
diff options
context:
space:
mode:
Diffstat (limited to 'coqpp')
-rw-r--r--coqpp/coqpp_main.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index d6ae0a7d6f..d5aedfcbb1 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -359,7 +359,6 @@ let print_atts_right fmt = function
let understand_state = function
| "close_proof" -> "VtCloseProof", false
- | "maybe_open_proof" -> "VtMaybeOpenProof", true
| "open_proof" -> "VtOpenProof", true
| "proof" -> "VtModifyProof", false
| "proof_opt_query" -> "VtReadProofOpt", false