From bea2a4f5fe5cab0abfc27492117c335a311a0c19 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 12 Jun 2013 21:07:40 +0000
Subject: Changing the type of Ltac values. Now they are toplevel generic
 arguments. That way we will be able to define interpretation of tactics
 without referring to tactic values.

Quite ad-hoc for now.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16574 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml  | 6 ++++++
 lib/util.mli | 8 ++++++++
 2 files changed, 14 insertions(+)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index c2d290714b..fb968cc64f 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -34,6 +34,12 @@ let is_blank = function
   | ' ' | '\r' | '\t' | '\n' -> true
   | _ -> false
 
+module Empty =
+struct
+  type t
+  let abort (x : t) = assert false
+end
+
 (* Strings *)
 
 module String : CString.ExtS = CString
diff --git a/lib/util.mli b/lib/util.mli
index 33812c2004..209f64c2f6 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -34,6 +34,14 @@ val is_digit : char -> bool
 val is_ident_tail : char -> bool
 val is_blank : char -> bool
 
+(** {6 Empty type} *)
+
+module Empty :
+sig
+  type t
+  val abort : t -> 'a
+end
+
 (** {6 Strings. } *)
 
 module String : CString.ExtS
-- 
cgit v1.2.3