From 8e257d43985e2775c8ff215ee97840a3cf6d14e5 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 4 Jul 2011 18:05:02 +0000
Subject: Extraction: in haskell, __ may have any type, no need to unsafeCoerce
 it

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14258 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/mlutil.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins')

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
-- 
cgit v1.2.3