From aa37087b8e7151ea96321a11012c1064210ef4ea Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 18 Dec 2012 17:09:31 +0000
Subject: Modulification of Label

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/setoid_ring/newring.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index d02d260074..c89e06f7c2 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -246,11 +246,11 @@ let my_constant c =
 let new_ring_path =
   Dir_path.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
 let ltac s =
-  lazy(make_kn (MPfile new_ring_path) (Dir_path.make []) (mk_label s))
+  lazy(make_kn (MPfile new_ring_path) (Dir_path.make []) (Label.make s))
 let znew_ring_path =
   Dir_path.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
-  lazy(make_kn (MPfile znew_ring_path) (Dir_path.make []) (mk_label s))
+  lazy(make_kn (MPfile znew_ring_path) (Dir_path.make []) (Label.make s))
 
 let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);;
 let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
@@ -829,7 +829,7 @@ let new_field_path =
   Dir_path.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
 
 let field_ltac s =
-  lazy(make_kn (MPfile new_field_path) (Dir_path.make []) (mk_label s))
+  lazy(make_kn (MPfile new_field_path) (Dir_path.make []) (Label.make s))
 
 
 let _ = add_map "field"
-- 
cgit v1.2.3