3 files changed, 6 insertions, 6 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 39826d744..89c2a0ae3 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -132,7 +132,7 @@ let rec add_labels mp = function
 exception Impossible
 
 let check_arity env cb =
-  let t = Typeops.type_of_constant_type env cb.const_type in
+  let t = cb.const_type in
   if Reduction.is_arity env t then raise Impossible
 
 let check_fix env cb i =
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 3661faada..661842790 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -518,7 +518,7 @@ and mlt_env env r = match r with
         match lookup_typedef kn cb with
         | Some _ as o -> o
         | None ->
-           let typ = Typeops.type_of_constant_type env cb.const_type
+           let typ = cb.const_type
            (* FIXME not sure if we should instantiate univs here *) in
 	   match flag_of_type env typ with
 	   | Info,TypeScheme ->
@@ -543,7 +543,7 @@ let record_constant_type env kn opt_typ =
   | Some schema -> schema
   | None ->
      let typ = match opt_typ with
-       | None -> Typeops.type_of_constant_type env cb.const_type
+       | None -> cb.const_type
        | Some typ -> typ
      in
      let mlt = extract_type env [] 1 typ [] in
@@ -969,7 +969,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
 
 let extract_constant env kn cb =
   let r = ConstRef kn in
-  let typ = Typeops.type_of_constant_type env cb.const_type in
+  let typ = cb.const_type in
   let warn_info () = if not (is_custom r) then add_info_axiom r in
   let warn_log () = if not (constant_has_body cb) then add_log_axiom r
   in
@@ -1025,7 +1025,7 @@ let extract_constant env kn cb =
 
 let extract_constant_spec env kn cb =
   let r = ConstRef kn in
-  let typ = Typeops.type_of_constant_type env cb.const_type in
+  let typ = cb.const_type in
   try
     match flag_of_type env typ with
     | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index f1bcde2f3..a4c2bcd88 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -120,7 +120,6 @@ let rec mgu = function
       mgu (a, a'); mgu (b, b')
   | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' ->
        List.iter mgu (List.combine l l')
-  | (Tdummy _, _ | _, Tdummy _) when lang() == Haskell -> ()
   | Tdummy _, Tdummy _ -> ()
   | Tvar i, Tvar j when Int.equal i j -> ()
   | Tvar' i, Tvar' j when  Int.equal i j -> ()
@@ -1052,6 +1051,7 @@ let rec simpl o = function
   | MLmagic(MLcase(typ,e,br)) ->
      let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in
      simpl o (MLcase(typ,e,br'))
+  | MLmagic(MLdummy _ as e) when lang () == Haskell -> e
   | MLmagic(MLexn _ as e) -> e
   | a -> ast_map (simpl o) a