From 67f5c70a480c95cfb819fc68439781b5e5e95794 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 14 Dec 2012 15:56:25 +0000
Subject: Modulification of identifier

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/quote/quote.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/quote')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 61a464c1c4..4238037e7a 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -189,10 +189,10 @@ let decomp_term c = kind_of_term (strip_outer_cast c)
   type [typ] *)
 
 let coerce_meta_out id =
-  let s = string_of_id id in
+  let s = Id.to_string id in
   int_of_string (String.sub s 1 (String.length s - 1))
 let coerce_meta_in n =
-  id_of_string ("M" ^ string_of_int n)
+  Id.of_string ("M" ^ string_of_int n)
 
 let compute_lhs typ i nargsi =
   match kind_of_term typ with
-- 
cgit v1.2.3