From 4425c8d353ffdcbed966c253f9624b550626ae0a Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 11 Mar 2013 20:14:31 +0000
Subject: Added a Local Definition vernacular command. This type of definition
 has to be refered through its qualified name even when the module containing
 it is imported.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16263 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 intf/decl_kinds.mli | 2 +-
 intf/vernacexpr.mli | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'intf')

diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli
index 91a03f6759..7111fd0555 100644
--- a/intf/decl_kinds.mli
+++ b/intf/decl_kinds.mli
@@ -8,7 +8,7 @@
 
 (** Informal mathematical status of declarations *)
 
-type locality = Local | Global
+type locality = Discharge | Local | Global
 
 type binding_kind = Explicit | Implicit
 
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 4655e3588d..a1eca85bc1 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -252,9 +252,9 @@ type vernac_expr =
       export_flag option * lreference list
   | VernacImport of export_flag * lreference list
   | VernacCanonical of reference or_by_notation
-  | VernacCoercion of locality * reference or_by_notation *
+  | VernacCoercion of locality_flag * reference or_by_notation *
       class_rawexpr * class_rawexpr
-  | VernacIdentityCoercion of locality * lident *
+  | VernacIdentityCoercion of locality_flag * lident *
       class_rawexpr * class_rawexpr
 
   (* Type classes *)
-- 
cgit v1.2.3