X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Facic_content%2FcicNotationPp.ml;h=fb38674dfb2cce12e406af6ab3b985b4964ffa8e;hb=63349b091357ba4cf3b9924bd1ffecd543f37252;hp=5dc6fd821c380f311a37005d5ed5057af33b2352;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index 5dc6fd821..fb38674df 100644
--- a/components/acic_content/cicNotationPp.ml
+++ b/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
@@ -247,12 +252,13 @@ let pp_params = function
       
 let pp_flavour = function
   | `Definition -> "Definition"
-  | `Fact -> "Fact"
-  | `Goal -> "Goal"
-  | `Lemma -> "Lemma"
-  | `Remark -> "Remark"
-  | `Theorem -> "Theorem"
-  | `Variant -> "Variant"
+  | `Fact -> "fact"
+  | `Goal -> "goal"
+  | `Lemma -> "lemma"
+  | `Remark -> "remark"
+  | `Theorem -> "theorem"
+  | `Variant -> "variant"
+  | `Axiom -> "axiom"
 
 let pp_fields fields =
   (if fields <> [] then "\n" else "") ^