diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index d8b7d364f1..8a0d1a05fe 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -105,6 +105,7 @@ let rec mgu = function mgu (a, a'); mgu (b, b') | Tglob (r,l), Tglob (r',l') when r = r' -> List.iter mgu (List.combine l l') + | (Tdummy _, _ | _, Tdummy _) when lang() = Haskell -> () | Tdummy _, Tdummy _ -> () | t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *) | _ -> raise Impossible |