From 25b07a6f824654be2041152d904507bc62102986 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 28 Feb 2018 13:45:04 +0100
Subject: Implement the Export Set/Unset feature.

This feature has been asked many times by different people, and allows to
have options in a module that are performed when this module is imported.

This supersedes the well-numbered cursed PR #313.
---
 library/goptions.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/goptions.mli')

diff --git a/library/goptions.mli b/library/goptions.mli
index 64015f42d..6c14d19ee 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -50,7 +50,7 @@ open Mod_subst
 
 type option_name = string list
 
-type option_locality = OptLocal | OptDefault | OptGlobal
+type option_locality = OptDefault | OptLocal | OptExport | OptGlobal
 
 (** {6 Tables. } *)
 
-- 
cgit v1.2.3