diff options
Diffstat (limited to 'plugins/extraction/mlutil.ml')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 3a70a50204..a4c2bcd883 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i*) -open API open Util open Names open Libnames @@ -121,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 -> () @@ -1053,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 |