fixed wrong calculation of free_metas

[helm.git] / helm / software / components / acic_content / cicNotationPp.ml

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index ee389022c5721097764d10f4fab34acf512d560f..590de7c5462f4fe5b097113f19ff20133da23a5d 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -171,9 +171,14 @@ and pp_pattern ((head, href, vars), term) =
 and pp_patterns patterns =
   sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns))
 
-and pp_capture_variable = function
+and pp_capture_variable = 
+  let clean s = 
+    let s = String.sub s 1 (String.length s - 1) in
+    String.sub s 0 (String.length s - 1) 
+  in
+  function
   | term, None -> pp_term term
-  | term, Some typ -> "(" ^ pp_term term ^ ": " ^ pp_term typ ^ ")"
+  | term, Some typ -> "(" ^ clean (pp_term term) ^ ": " ^ pp_term typ ^ ")"
 
 and pp_box_spec (kind, spacing, indent) =
   let int_of_bool b = if b then 1 else 0 in