commented out a line to help paramodulation.

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

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index 5dc6fd821c380f311a37005d5ed5057af33b2352..590de7c5462f4fe5b097113f19ff20133da23a5d 100644 (file)
--- 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,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 "") ^