diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-03 13:12:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-03 13:12:03 +0000 |
| commit | b82cb93d2020783f72a8f99142799b51ca7991a9 (patch) | |
| tree | a641aabeae358adac2dddda2ea121528f17ad293 /lib/util.mli | |
| parent | 8529f5bdf888ac982d359065015295306ec98384 (diff) | |
Added multiple implicit arguments rules per name.
Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]".
This should a priori be used with care (it might be a bit disturbing
seeing the same constant used with apparently incompatible signatures).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/util.mli')
| -rw-r--r-- | lib/util.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/util.mli b/lib/util.mli index 83fac5fcd..13be5521d 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -348,7 +348,9 @@ val prlist_with_sep : val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds val prvect_with_sep : - (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds + (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds +val prvecti_with_sep : + (unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds |