Previously, small_delta_step would occasionally return two machines in
normal form, with a false "are_normal" flag: this in turn caused
unif_machines to perform more steps than necessary. Now the flag returned
by small_delta_step is true iff it could not perform any reduction step;
therefore unif_machines won't try a recursive call on the new machines
(which are equal to the old ones).
pp (lazy("DELTA STEP TO: " ^ string_of_int delta));
let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in
let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in
pp (lazy("DELTA STEP TO: " ^ string_of_int delta));
let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in
let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in
- m1', m2', (m1 == m1' && m2 == m2') || delta = 0
- else m1', m2', delta = 0
+ m1', m2', (m1 == m1' && m2 == m2') (* || delta = 0 *)
+ else m1', m2', (m1 == m1' && m2 == m2') (* delta = 0 *)
in
let rec unif_machines metasenv subst =
function
in
let rec unif_machines metasenv subst =
function
in
try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
with UnificationFailure _ | Uncertain _ when not are_normal ->
in
try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
with UnificationFailure _ | Uncertain _ when not are_normal ->
- unif_machines metasenv subst (small_delta_step m1 m2)
+ let m1,m2,normal as small = small_delta_step m1 m2 in
+ if not normal then unif_machines metasenv subst small
+ else raise (UnificationFailure (lazy "TEST x"))
(* (*D*) in outside(); rc with exn -> outside (); raise exn *)
in
try fo_unif test_eq_only metasenv subst t1 t2
(* (*D*) in outside(); rc with exn -> outside (); raise exn *)
in
try fo_unif test_eq_only metasenv subst t1 t2