X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=590de7c5462f4fe5b097113f19ff20133da23a5d;hb=942023d1f147318b7869f40fb1556c2d69f3d731;hp=5dc6fd821c380f311a37005d5ed5057af33b2352;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 5dc6fd821..590de7c54 100644
--- 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
@@ -247,12 +252,12 @@ 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"
 
 let pp_fields fields =
   (if fields <> [] then "\n" else "") ^