From 011ac2d7db53f0df2849985ef9cc044574c0ddb0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 Apr 2016 16:44:42 +0200 Subject: Switching to an untyped toplevel representation for Ltac values. --- lib/genarg.mli | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'lib/genarg.mli') diff --git a/lib/genarg.mli b/lib/genarg.mli index 93665fd45..04113ae28 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -96,11 +96,17 @@ sig | Opt : 'a tag -> 'a option tag | Pair : 'a tag * 'b tag -> ('a * 'b) tag - type t = Dyn : 'a tag * 'a -> t + type t = Dyn : 'a typ * 'a -> t - val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option + val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option val repr : 'a typ -> string - val pr : 'a tag -> Pp.std_ppcmds + val pr : 'a typ -> Pp.std_ppcmds + + val list_tag : t list typ + val opt_tag : t option typ + val pair_tag : (t * t) typ + + val inject : 'a tag -> 'a -> t end (** Dynamic types for toplevel values. While the generic types permit to relate -- cgit v1.2.3