exception AssertFailure of string Lazy.t;;
+let debug = ref false;;
+let pp m = if !debug then prerr_endline (Lazy.force m) else ();;
+
module type Strategy = sig
type stack_term
type env_term
when (Ref.eq r1 r2 &&
List.length (E.get_relevance r1) >= List.length tl1) ->
let relevance = E.get_relevance r1 in
+(* if the types were convertible the following optimization is sound
let relevance = match r1 with
| Ref.Ref (_,Ref.Con (_,_,lno)) ->
let _,relevance = HExtlib.split_nth lno relevance in
HExtlib.mk_list false lno @ relevance
| _ -> relevance
in
+*)
(try
HExtlib.list_forall_default3_var
(fun t1 t2 b -> not b || aux true context t1 t2 )