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

---
 plugins/ltac/tauto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac/tauto.ml')

diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 13492ed51c..5eacb1a95e 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -197,7 +197,7 @@ let flatten_contravariant_disj _ ist =
 
 let make_unfold name =
   let dir = DirPath.make (List.map Id.of_string ["Logic"; "Init"; "Coq"]) in
-  let const = Constant.make2 (MPfile dir) (Label.make name) in
+  let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in
   (Locus.AllOccurrences, ArgArg (EvalConstRef const, None))
 
 let u_iff = make_unfold "iff"
-- 
cgit v1.2.3