diff options
| author | Gaëtan Gilbert | 2018-10-11 19:08:33 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-02 13:26:16 +0100 |
| commit | c44080b74f4ea1e4b7ae88dfe5a440364bed3fca (patch) | |
| tree | a14664e5bb5165415d2b1928fc0f2896e6ec36c1 /stm | |
| parent | 1808904b3088595f89c24aa25bffcc54b2b48fda (diff) | |
Universe Polymorphism is a normal attribute modulo the stm (no Flags)
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 2 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 16 |
2 files changed, 9 insertions, 9 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 07049815ef..cfadada104 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2133,7 +2133,7 @@ and Reach : sig end = struct (* {{{ *) let async_policy () = - if Flags.is_universe_polymorphism () then false + if Attributes.is_universe_polymorphism () then false else if VCS.is_interactive () = `Yes then (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy) else diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f3961327d8..c93487d377 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -50,7 +50,7 @@ let idents_of_name : Names.Name.t -> Names.Id.t list = let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"] let options_affecting_stm_scheduling = - [ Vernacentries.universe_polymorphism_option_name; + [ Attributes.universe_polymorphism_option_name; stm_allow_nested_proofs_option_name ] let classify_vernac e = @@ -192,15 +192,15 @@ let classify_vernac e = try Vernacentries.get_vernac_classifier s l with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in - let rec static_control_classifier ~poly = function + let rec static_control_classifier = function | VernacExpr (f, e) -> - let poly' = Attributes.(parse_drop_extra polymorphic_nowarn f) in - static_classifier ~poly:(Option.default poly poly') e - | VernacTimeout (_,e) -> static_control_classifier ~poly e + let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in + static_classifier ~poly e + | VernacTimeout (_,e) -> static_control_classifier e | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) -> - static_control_classifier ~poly e + static_control_classifier e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) - (match static_control_classifier ~poly e with + (match static_control_classifier e with | ( VtQuery | VtProofStep _ | VtSideff _ | VtProofMode _ | VtMeta), _ as x -> x | VtQed _, _ -> @@ -208,7 +208,7 @@ let classify_vernac e = VtNow | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) in - static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e + static_control_classifier e let classify_as_query = VtQuery, VtLater let classify_as_sideeff = VtSideff [], VtLater |