aboutsummaryrefslogtreecommitdiff
path: root/parsing/stdlib.mli
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/stdlib.mli')
-rw-r--r--parsing/stdlib.mli15
1 files changed, 15 insertions, 0 deletions
diff --git a/parsing/stdlib.mli b/parsing/stdlib.mli
new file mode 100644
index 0000000000..7bb890d18d
--- /dev/null
+++ b/parsing/stdlib.mli
@@ -0,0 +1,15 @@
+
+(* $Id$ *)
+
+open Term
+
+(*s This module collects the global references of the standard library
+ used in ocaml files *)
+
+(* Natural numbers *)
+val glob_nat : global_reference
+val glob_O : global_reference
+val glob_S : global_reference
+
+(* Special variable for pretty-printing of constant naturals *)
+val glob_My_special_variable_nat : global_reference