(**** Signature minimale pour le TP 2 et 1 ****)

type symbol
type var
type term
type subst

exception No_Unify
exception No_Match

val contains : var -> subst -> bool

val substitute : subst -> term -> term
val occurs : var -> term -> bool

val unify :(term * term) list -> subst

val match : (term * term) list -> subst

val create_example_of_unification_problem : int -> (term * term) list


(**** Signature minimale pour le TP 3 ****)

open Tree
(* open Dag *)

type tuple
type order_symbol
type order
type status

val lex : order -> int list -> tuple -> tuple -> bool
val mul : order -> tuple -> tuple -> bool
val lpo : order_symbol -> order
val rpo : order_symbol -> status -> order

val is_inf : order -> term -> term -> bool
val is_inf_symbol : order_symbol -> symbol -> symbol -> bool

(**** Signature minimale pour le TP 4 ****)

open Tree
(* open Dag *)

val critical_pairs : (term * term) list -> (term * term) list