From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001
From: Matej Košík <matej.kosik@inria.fr>
Date: Mon, 29 May 2017 11:02:06 +0200
Subject: Remove (useless) aliases from the API.

---
 plugins/romega/const_omega.ml | 7 ++++---
 plugins/romega/g_romega.ml4   | 2 +-
 2 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'plugins/romega')

diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 4db4bdc2c..06c80a825 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -7,6 +7,7 @@
  *************************************************************************)
 
 open API
+open Names
 
 let module_refl_name = "ReflOmegaCore"
 let module_refl_path = ["Coq"; "romega"; module_refl_name]
@@ -39,7 +40,7 @@ let destructurate t =
   | Term.Ind (isp,_), args ->
      Kapp (string_of_global (Globnames.IndRef isp), args)
   | Term.Var id, [] -> Kvar(Names.Id.to_string id)
-  | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
+  | Term.Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
   | _ -> Kufo
 
 exception DestConstApp
@@ -244,7 +245,7 @@ let minus = lazy (z_constant "Z.sub")
 let recognize_pos t =
   let rec loop t =
     let f,l = dest_const_apply t in
-    match Names.Id.to_string f,l with
+    match Id.to_string f,l with
     | "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t))
     | "xO",[t] -> Bigint.mult Bigint.two (loop t)
     | "xH",[] -> Bigint.one
@@ -255,7 +256,7 @@ let recognize_pos t =
 let recognize_Z t =
   try
     let f,l = dest_const_apply t in
-    match Names.Id.to_string f,l with
+    match Id.to_string f,l with
     | "Zpos",[t] -> recognize_pos t
     | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos t)
     | "Z0",[] -> Some Bigint.zero
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 30d93654b..53f6f42c8 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -19,7 +19,7 @@ open Stdarg
 
 let eval_tactic name =
   let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
-  let kn = KerName.make2 (MPfile dp) (Label.make name) in
+  let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in
   let tac = Tacenv.interp_ltac kn in
   Tacinterp.eval_tactic tac
 
-- 
cgit v1.2.3