diff options
| author | Maxime Dénès | 2018-07-26 11:47:33 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-07-26 11:47:33 +0200 |
| commit | 09c76adaff7adaada1c49479dfa9a4d0a4b416af (patch) | |
| tree | c59ff9f4ff5ca8c31f746b5d47618fd70085e621 /stm | |
| parent | 3f2979c5f0fc289f41cc0e36b9914b3c8f7f77c5 (diff) | |
| parent | b9ff36b39eb193757ce57a89afe138cd09e759d7 (diff) | |
Merge PR #8050: Cleanup VERNAC EXTEND
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/vernac_classifier.ml | 9 | ||||
| -rw-r--r-- | stm/vernac_classifier.mli | 5 |
2 files changed, 1 insertions, 13 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 6be80d29a5..eca0c6674b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -42,13 +42,6 @@ let string_of_vernac_when = function let string_of_vernac_classification (t,w) = string_of_vernac_type t ^ " " ^ string_of_vernac_when w -let classifiers = ref [] -let declare_vernac_classifier - (s : Vernacexpr.extend_name) - (f : Genarg.raw_generic_argument list -> unit -> vernac_classification) -= - classifiers := !classifiers @ [s,f] - let idents_of_name : Names.Name.t -> Names.Id.t list = function | Names.Anonymous -> [] @@ -194,7 +187,7 @@ let classify_vernac e = | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> - try List.assoc s !classifiers l () + 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 diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index 45fbfb42af..e82b191418 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -9,17 +9,12 @@ (************************************************************************) open Vernacexpr -open Genarg val string_of_vernac_classification : vernac_classification -> string (** What does a vernacular do *) val classify_vernac : vernac_control -> vernac_classification -(** Install a vernacular classifier for VernacExtend *) -val declare_vernac_classifier : - Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit - (** Standard constant classifiers *) val classify_as_query : vernac_classification val classify_as_sideeff : vernac_classification |