diff options
Diffstat (limited to 'plugins/firstorder/unify.ml')
| -rw-r--r-- | plugins/firstorder/unify.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 2556460f5..f7ee9fdad 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -78,7 +78,7 @@ let unif t1 t2= for i=0 to l-1 do Queue.add (va.(i),vb.(i)) bige done - | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2)) + | _->if not (eq_constr_nounivs nt1 nt2) then raise (UFAIL (nt1,nt2)) done; assert false (* this place is unreachable but needed for the sake of typing *) |