aboutsummaryrefslogtreecommitdiff
path: root/ide/ideutils.mli
diff options
context:
space:
mode:
authormonate2003-09-19 08:48:38 +0000
committermonate2003-09-19 08:48:38 +0000
commitdf0bf4b7226efb91b462221ca16463b7f5e93339 (patch)
tree28ed9422399c73c3f7e712bc45340a73ba8f666e /ide/ideutils.mli
parentcc9660a305171191a1446818a380a8f58c824f55 (diff)
Coqide : les nouveaute d'aout
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4424 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/ideutils.mli')
-rw-r--r--ide/ideutils.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 6c2124a374..bf19159789 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -48,7 +48,10 @@ val print_list : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
val run_command : (string -> unit) -> string -> Unix.process_status*string
+
+val prime : Glib.unichar
val underscore : Glib.unichar
+val arobase : Glib.unichar
val bn : Glib.unichar
val space : Glib.unichar
val tab : Glib.unichar