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.
---
 interp/dumpglob.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 13ed65056d..0197cf9ae2 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -72,7 +72,7 @@ open Decl_kinds
 let type_of_logical_kind = function
   | IsDefinition def ->
       (match def with
-      | Definition -> "def"
+      | Definition | Let -> "def"
       | Coercion -> "coe"
       | SubClass -> "subclass"
       | CanonicalStructure -> "canonstruc"
-- 
cgit v1.2.3