From 368a25e4ef14512b00f5799e26c3f615bc540201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 22 May 2018 00:07:26 +0200 Subject: [api] Misctypes removal: several moves: - move_location to proofs/logic. - intro_pattern_naming to Namegen. --- plugins/funind/indfun.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index efbd029e4..cd640eebd 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -10,7 +10,7 @@ open Libnames open Globnames open Glob_term open Declarations -open Misctypes +open Tactypes open Decl_kinds module RelDecl = Context.Rel.Declaration @@ -782,7 +782,7 @@ let rec add_args id new_args = CAst.map (function | CSort _ as b -> b | CCast(b1,b2) -> CCast(add_args id new_args b1, - Miscops.map_cast_type (add_args id new_args) b2) + Glob_ops.map_cast_type (add_args id new_args) b2) | CRecord pars -> CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars) | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.") -- cgit v1.2.3