Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 15 insertions, 0 deletions

diff --git a/contrib/jprover/opname.mli b/contrib/jprover/opname.mli
new file mode 100644
index 00000000..56bf84e2
--- /dev/null
+++ b/contrib/jprover/opname.mli
@@ -0,0 +1,15 @@
+(* This module is extracted from Meta-Prl. *)
+
+type token = string
+and atom = string list
+val opname_token : token
+type opname = {
+  mutable opname_token : token;
+  mutable opname_name : string list;
+} 
+val nil_opname : opname
+val mk_opname : string -> opname -> opname
+val make_opname : string list -> opname
+val eq : opname -> opname -> bool
+val dest_opname : opname -> string list
+val string_of_opname : opname -> string