diff --git a/src/ltac_iter_plugin.ml4 b/src/ltac_iter_plugin.ml4 index 9413575..07508c4 100644 --- a/src/ltac_iter_plugin.ml4 +++ b/src/ltac_iter_plugin.ml4 @@ -5,7 +5,6 @@ open Ltac_plugin open Tacexpr open Tacinterp -open Misctypes open Tacarg @@ -23,14 +22,14 @@ struct let ltac_lcall tac args = let (location, name) = Loc.tag (Names.Id.of_string tac) in Tacexpr.TacArg(Loc.tag @@ Tacexpr.TacCall - (Loc.tag (Misctypes.ArgVar (CAst.make ?loc:location name),args))) + (Loc.tag (Locus.ArgVar (CAst.make ?loc:location name),args))) let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) = let open Names in let fold arg (i, vars, lfun) = let id = Id.of_string ("x" ^ string_of_int i) in let (l,n) = (Loc.tag id) in - let x = Reference (ArgVar (CAst.make ?loc:l n)) in + let x = Reference (Locus.ArgVar (CAst.make ?loc:l n)) in (succ i, x :: vars, Id.Map.add id arg lfun) in let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in @@ -124,7 +123,7 @@ struct (Proofview.Goal.hyps gl) end | c -> - CErrors.user_err ~label:"WithHintDb" + CErrors.user_err ~hdr:"WithHintDb" Pp.( str "Not Implemented: " ++ pr_collection c) in resolve_collection