Commit 0c1420e1 authored by Martin Clochard's avatar Martin Clochard

first_order_matching: prevent quantifier matching from raising Invalid_argument

parent 2670d6f9
......@@ -362,9 +362,11 @@ let first_order_matching (vars : Svs.t) (largs : term list)
let (vl1, _tl1, term1) = t_open_quant bv1 in
let (vl2, _tl2, term2) = t_open_quant bv2 in
let (mt, mv) =
List.fold_left2 (fun (mt, mv) e1 e2 ->
try List.fold_left2 (fun (mt, mv) e1 e2 ->
let mt = Ty.ty_match mt e1.vs_ty e2.vs_ty in
(mt, Mvs.add e1 (t_var e2) mv)) (mt, mv) vl1 vl2 in
(mt, Mvs.add e1 (t_var e2) mv)) (mt, mv) vl1 vl2
with Invalid_argument _ -> raise (NoMatch (Some (t1,t2)))
in
loop (mt, mv) (T term1 :: r1) (T term2 :: r2)
| _ -> raise (NoMatch (Some (t1, t2)))
end
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment