diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-13 16:44:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-04 13:47:12 +0200 |
| commit | 011ac2d7db53f0df2849985ef9cc044574c0ddb0 (patch) | |
| tree | 57a60e8a95705b61c7d45fd807f05c0384f56e8f /lib/genarg.mli | |
| parent | 5da0f107cb3332d5cd87fc352aef112f6b74fc97 (diff) | |
Switching to an untyped toplevel representation for Ltac values.
Diffstat (limited to 'lib/genarg.mli')
| -rw-r--r-- | lib/genarg.mli | 12 |
1 files changed, 9 insertions, 3 deletions
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 |