From 88a16f49efd315aa1413da67f6d321a5fe269772 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 17 Jan 2016 01:46:02 +0100
Subject: Simplification and type-safety of Pcoq thanks to GADTs in Genarg.

---
 lib/genarg.ml  | 10 ----------
 lib/genarg.mli |  3 ---
 2 files changed, 13 deletions(-)

(limited to 'lib')

diff --git a/lib/genarg.ml b/lib/genarg.ml
index 030797da9c..6c10dee2ae 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -194,16 +194,6 @@ type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
 type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
 type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type
 
-let arg_list : type l. (_, l) abstract_argument_type -> (_, l) abstract_argument_type = function
-| Rawwit t -> Rawwit (ListArg t)
-| Glbwit t -> Glbwit (ListArg t)
-| Topwit t -> Topwit (ListArg t)
-
-let arg_opt : type l. (_, l) abstract_argument_type -> (_, l) abstract_argument_type = function
-| Rawwit t -> Rawwit (OptArg t)
-| Glbwit t -> Glbwit (OptArg t)
-| Topwit t -> Topwit (OptArg t)
-
 type ('a, 'b, 'c, 'l) cast =
 | Rcast : 'a -> ('a, 'b, 'c, rlevel) cast
 | Gcast : 'b -> ('a, 'b, 'c, glevel) cast
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 38dc0c684a..a1b74c6744 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -291,9 +291,6 @@ val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) gena
 val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
   ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
 
-val arg_list : ('a, 'l) abstract_argument_type -> ('a list, 'l) abstract_argument_type
-val arg_opt : ('a, 'l) abstract_argument_type -> ('a option, 'l) abstract_argument_type
-
 (** {5 Magic used by the parser} *)
 
 val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option
-- 
cgit v1.2.3