Commit edd05951 authored by Martin Clochard's avatar Martin Clochard

compute: another bugfix

parent a78ba0cb
...@@ -338,24 +338,9 @@ let first_order_matching (vars : Svs.t) (largs : term list) ...@@ -338,24 +338,9 @@ let first_order_matching (vars : Svs.t) (largs : term list)
end end
| _ -> raise NoMatch | _ -> raise NoMatch
end end
| _ -> | (Tconst _ | Ttrue | Tfalse) when t_equal t1 t2 ->
(* loop sigma r1 r2
Format.eprintf "are these terms equal ?..."; | _ -> raise NoMatch
*)
if t_equal t1 t2 then
begin
(*
Format.eprintf " yes!@.";
*)
loop sigma r1 r2
end
else
begin
(*
Format.eprintf " no@.";
*)
raise NoMatch
end
end end
| _ -> raise NoMatch | _ -> raise NoMatch
in in
......
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