removing warnings.

gmalecha · Apr 19, 2019 · 3dbe87d · 3dbe87d
1 parent 9e53dc0
commit 3dbe87d
Showing 1 changed file with 3 additions and 4 deletions.
diff --git 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