1 files changed, 0 insertions, 110 deletions
diff --git a/contrib/jprover/jterm.mli b/contrib/jprover/jterm.mli
deleted file mode 100644
index 0bc42010..00000000
--- a/contrib/jprover/jterm.mli
+++ /dev/null
@@ -1,110 +0,0 @@
-(* This module is modified and extracted from Meta-Prl. *)
-
-(* Definitions of [jterm]: *)
-type param = param'
-and operator = operator'
-and term = term'
-and bound_term = bound_term'
-and param' =
-  | Number of int
-  | String of string
-  | Token of string
-  | Var of string
-  | ParamList of param list
-and operator' = { op_name : Opname.opname; op_params : param list; } 
-and term' = { term_op : operator; term_terms : bound_term list; } 
-and bound_term' = { bvars : string list; bterm : term; } 
-type term_subst = (string * term) list
-
-type error_msg = TermMatchError of term * string | StringError of string
-
-exception RefineError of string * error_msg
-
-(* Collect free variables: *)
-val free_vars_list : term -> string list
-
-(* Substitutions: *)
-val subst_term : term list -> string list list -> string list -> term -> term
-val subst : term -> string list -> term list -> term
-val subst1 : term -> string -> term -> term
-val var_subst : term -> term -> string -> term
-val apply_subst : term -> (string * term) list -> term
-
-(* Unification: *)
-val unify_mm : term -> term -> 'a -> (string * term) list
-
-val xnil_term : term'
-
-(* Testing functions: *)
-val is_xnil_term : term' -> bool
-val is_var_term : term' -> bool
-val is_true_term : term' -> bool
-val is_false_term : term' -> bool
-val is_all_term : term' -> bool
-val is_exists_term : term' -> bool
-val is_or_term : term' -> bool
-val is_and_term : term' -> bool
-val is_cor_term : term' -> bool
-val is_cand_term : term' -> bool
-val is_implies_term : term' -> bool
-val is_iff_term : term' -> bool
-val is_not_term : term' -> bool
-val is_fun_term : term -> bool
-val is_const_term : term -> bool
-
-
-(* Constructors for [jterms]: *)
-val var_ : string -> term'
-val fun_ : string -> term list -> term'
-val const_ : string -> term'
-val pred_ : string -> term list -> term'
-val not_ : term -> term'
-val and_ : term -> term -> term'
-val or_ : term -> term -> term'
-val imp_ : term -> term -> term'
-val cand_ : term -> term -> term'
-val cor_ : term -> term -> term'
-val iff_ : term -> term -> term'
-val false_ : term'
-val true_ : term'
-val nil_term : term'
-val forall : string -> term -> term'
-val exists : string -> term -> term'
-
-
-(* Destructors for [jterm]: *)
-val dest_var : term -> string
-val dest_fun : term -> string * term list
-val dest_const : term -> string
-val dest_not : term -> term
-val dest_iff : term -> term * term
-val dest_implies : term -> term * term
-val dest_cand : term -> term * term
-val dest_cor : term -> term * term
-val dest_and : term -> term * term
-val dest_or : term -> term * term
-val dest_exists : term -> string * term * term
-val dest_all : term -> string * term * term
-
-(* Wide-logical connectives: *)
-val wand_ : term list -> term
-val wor_ : term list -> term
-val wimp_ : term list -> term
-
-(* Printing and debugging tools: *)
-val fprint_str_list : out_channel -> string list -> unit
-val mbreak : string -> unit
-val print_strs : string list -> unit
-val print_term : out_channel -> term -> unit
-val print_error_msg : exn -> unit
-
-(* Other exported functions for [jall.ml]: *)
-val make_term : 'a -> 'a
-val dest_term : 'a -> 'a
-val make_op : 'a -> 'a
-val dest_op : 'a -> 'a
-val make_bterm : 'a -> 'a
-val dest_bterm : 'a -> 'a
-val dest_param : 'a -> 'a
-val mk_var_term : string -> term'
-val mk_string_term : Opname.opname -> string -> term'