aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/goptionstyp.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/goptionstyp.mli')
-rw-r--r--library/goptionstyp.mli26
1 files changed, 0 insertions, 26 deletions
diff --git a/library/goptionstyp.mli b/library/goptionstyp.mli
deleted file mode 100644
index 541a1470c..000000000
--- a/library/goptionstyp.mli
+++ /dev/null
@@ -1,26 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(** Some types used in the generic option mechanism (Goption) *)
-
-(** Placing them here in a pure interface avoid some dependency issues
- when compiling CoqIDE *)
-
-type option_name = string list
-
-type option_value =
- | BoolValue of bool
- | IntValue of int option
- | StringValue of string
-
-type option_state = {
- opt_sync : bool;
- opt_depr : bool;
- opt_name : string;
- opt_value : option_value;
-}