From 3bbeb996b9c699eb841a7c56aa07c670fa7cea92 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 6 Jun 2013 15:26:05 +0000
Subject: More comments in Genarg.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16565 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 intf/tacexpr.mli    | 8 --------
 intf/vernacexpr.mli | 2 +-
 2 files changed, 1 insertion(+), 9 deletions(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 719cf0d33b..dbe8887149 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -270,15 +270,7 @@ type raw_tactic_arg =
 
 (** Misc *)
 
-type raw_generic_argument = rlevel generic_argument
-type glob_generic_argument = glevel generic_argument
-type typed_generic_argument = tlevel generic_argument
-
 type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
 type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
 
-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
-
 type 'a declaration_hook = locality -> global_reference -> 'a
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index b311b770db..138ef5cbbe 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -398,7 +398,7 @@ type vernac_expr =
   | VernacToplevelControl of exn
 
   (* For extension *)
-  | VernacExtend of string * raw_generic_argument list
+  | VernacExtend of string * Genarg.raw_generic_argument list
 
   (* Flags *)
   | VernacProgram of vernac_expr
-- 
cgit v1.2.3