let rec compare t1 t2 = match t1, t2 with | Const c1, Const c2 -> compare_constants c1 c2 | Const _, _ -> -1 | _, Const _ -> 1 | Elem (_, (Constr | Var)), Elem (_, Glob) -> -1 | Elem (_, Glob), Elem (_, (Constr | Var)) -> 1 | Elem (s1, _), Elem (s2, _) -> Hstring.compare s1 s2 | Elem _, _ -> -1 | _, Elem _ -> 1 | Access (a1, l1), Access (a2, l2) -> let c = Hstring.compare a1 a2 in if c<>0 then c else Hstring.compare_list l1 l2 | Access _, _ -> -1 | _, Access _ -> 1 | Arith (t1, cs1), Arith (t2, cs2) -> let c = compare t1 t2 in if c<>0 then c else compare_constants cs1 cs2