From ae5944b360c1e181fa162d7d6dced7e671c6fbe6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 12 Sep 2017 17:26:53 +0200 Subject: Remove "obsolete_locality" and fix STM vernac classification. We remove deprecated syntax "Coercion Local" and such, and seize the opportunity to refactor some code around vernac_expr. We also do a small fix on the STM classification, which didn't know about Let Fixpoint and Let CoFixpoint. This is a preliminary step for the work on attributes. --- library/kindops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/kindops.mli') diff --git a/library/kindops.mli b/library/kindops.mli index 77979c915..06f873e85 100644 --- a/library/kindops.mli +++ b/library/kindops.mli @@ -12,4 +12,4 @@ open Decl_kinds val logical_kind_of_goal_kind : goal_object_kind -> logical_kind val string_of_theorem_kind : theorem_kind -> string -val string_of_definition_kind : definition_kind -> string +val string_of_definition_object_kind : definition_object_kind -> string -- cgit v1.2.3