diff options
| author | Gaëtan Gilbert | 2019-04-01 13:44:54 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-04-12 13:59:23 +0200 |
| commit | 839ed4e80ca4dc068422c7c9fdb0c00e4ff1ebab (patch) | |
| tree | 37a4e9a4b9d291d630f63eb37f7307f91fe65d60 /stm/vernac_classifier.ml | |
| parent | 38b86f40b3e2c6ce0ea77c94cf0c48efbf7c9f13 (diff) | |
Unify Set and Unset handling for options
Not sure if the idetop.set_options was correctly changed, ocaml types
pass at least.
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 58fe923f9e..243b5c333d 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -57,6 +57,7 @@ let options_affecting_stm_scheduling = stm_allow_nested_proofs_option_name; Vernacentries.proof_mode_opt_name; Attributes.program_mode_option_name; + Proof_using.proof_using_opt_name; ] let classify_vernac e = @@ -64,7 +65,7 @@ let classify_vernac e = (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) - | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l)) + | VernacSetOption (_, l,_) when CList.exists (CList.equal String.equal l) options_affecting_stm_scheduling -> VtSideff [], VtNow @@ -91,9 +92,6 @@ let classify_vernac e = VtProofStep { parallel = `No; proof_block_detection = Some "curly" }, VtLater - (* Options changing parser *) - | VernacUnsetOption (_, ["Default";"Proof";"Using"]) - | VernacSetOption (_, ["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) -> VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater @@ -156,7 +154,7 @@ let classify_vernac e = | VernacReserve _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ - | VernacUnsetOption _ | VernacSetOption _ + | VernacSetOption _ | VernacAddOption _ | VernacRemoveOption _ | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ |