Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 6 insertions, 3 deletions

diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index e0a6cba3..7cd22a36 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: quote.ml 9178 2006-09-26 11:18:22Z barras $ *)
+(* $Id: quote.ml 10790 2008-04-14 22:34:19Z herbelin $ *)
 
 (* The `Quote' tactic *)
 
@@ -191,8 +191,11 @@ let decomp_term c = kind_of_term (strip_outer_cast c)
   ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive
   type [typ] *)
 
-let coerce_meta_out id = int_of_string (string_of_id id)
-let coerce_meta_in n = id_of_string (string_of_int n)
+let coerce_meta_out id = 
+  let s = string_of_id 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)
 
 let compute_lhs typ i nargsi =
   match kind_of_term typ with