exception AssertFailure of string Lazy.t;;
let debug = ref false;;
-let pp m = if !debug then prerr_endline (Lazy.force m) else ();;
+(*let pp m = if !debug then prerr_endline (Lazy.force m) else ();;*)
module type Strategy = sig
type stack_term
let whd = R.whd
-let (===) x y = Pervasives.compare x y = 0 ;;
+let (===) x y = Stdlib.compare x y = 0 ;;
let get_relevance = ref (fun _ ~metasenv:_ ~subst:_ _ _ -> assert false);;
(is_prop || aux test_eq_only context term1 term2) &&
(try List.for_all2 (aux test_eq_only context) pl1 pl2
with Invalid_argument _ -> false)
- | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+ | (C.Implicit _, _) | (_, C.Implicit _) -> true
+ (* CSC: was assert false, but it happens when looking for coercions
+ during pretty printing of terms yet to be refined *)
| (_,_) -> false
;;
R.reduce status ~delta ~subst context m2
in
let rec convert_machines test_eq_only
- ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2), norm2 as m2)
+ (((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2), norm2 as m2))
=
(alpha_eq status test_eq_only
(R.unwind status (k1,e1,t1,[])) (R.unwind status (k2,e2,t2,[])) &&