diff options
| author | Pierre-Marie Pédrot | 2018-11-05 14:31:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-05 14:31:40 +0100 |
| commit | 9c2c0006d1a3ce8e536ede2468546142bf96bca5 (patch) | |
| tree | 73ab2e2c29b7f388ccf701a30032bcfbd360bb98 /stm | |
| parent | ea678521c9eda7acde3a0276e0cec0931dbc6416 (diff) | |
| parent | ae21dd604137c2e361adc0ba18ffebef27bc5eb2 (diff) | |
Merge PR #8515: Command driven attributes
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 3 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 15 |
2 files changed, 9 insertions, 9 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index b731678f6d..514b364af3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1077,6 +1077,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t | _ -> false in let aux_interp st expr = + (* XXX unsupported attributes *) let cmd = Vernacprop.under_control expr in if is_filtered_command cmd then (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) @@ -2132,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 85babd922b..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,16 +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 _, atts = Vernacentries.attributes_of_flags f Vernacinterp.(mk_atts ~polymorphic:poly ()) in - let poly = atts.Vernacinterp.polymorphic in + let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in static_classifier ~poly e - | VernacTimeout (_,e) -> static_control_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 _, _ -> @@ -209,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 |