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.
---
 intf/decl_kinds.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'intf/decl_kinds.ml')

diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
index a977588332..1dea6d9e98 100644
--- a/intf/decl_kinds.ml
+++ b/intf/decl_kinds.ml
@@ -8,6 +8,8 @@
 
 (** Informal mathematical status of declarations *)
 
+type discharge = DoDischarge | NoDischarge
+
 type locality = Discharge | Local | Global
 
 type binding_kind = Explicit | Implicit
@@ -40,6 +42,7 @@ type definition_object_kind =
   | IdentityCoercion
   | Instance
   | Method
+  | Let
 
 type assumption_object_kind = Definitional | Logical | Conjectural
 
-- 
cgit v1.2.3