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

1 files changed, 8 insertions, 0 deletions

diff --git a/lib/util.mli b/lib/util.mli
index 33812c200..209f64c2f 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