diff options
Diffstat (limited to 'contrib/ring/quote.ml')
| -rw-r--r-- | contrib/ring/quote.ml | 9 |
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 |