diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/haskell.ml | 3 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 4 |
2 files changed, 3 insertions, 4 deletions
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index f708307c38..28abb7f575 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -58,7 +58,6 @@ let preamble mod_name comment used_modules usf = else str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ str "import qualified GHC.Base" ++ fnl () ++ - str "import qualified GHC.Prim" ++ fnl () ++ str "#else" ++ fnl () ++ str "-- HUGS" ++ fnl () ++ str "import qualified IOExts" ++ fnl () ++ @@ -78,7 +77,7 @@ let preamble mod_name comment used_modules usf = (if not usf.tunknown then mt () else str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ - str "type Any = GHC.Prim.Any" ++ fnl () ++ + str "type Any = GHC.Base.Any" ++ fnl () ++ str "#else" ++ fnl () ++ str "-- HUGS" ++ fnl () ++ str "type Any = ()" ++ fnl () ++ diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 705a51edd3..c63492d1be 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Pp open CErrors open Util +open Names open Nameops open Namegen open Constr @@ -1143,7 +1143,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = (* | _ -> b') *) | Lambda (n, t, b) when flags.under_lambdas -> - let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in + let n' = Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env) n in let open Context.Rel.Declaration in let env' = EConstr.push_rel (LocalAssum (n', t)) env in let bty = Retyping.get_type_of env' (goalevars evars) b in |