From 213039eee2048bc1da423345c5c1e05a1e775f99 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 22 Nov 2007 14:32:30 +0000
Subject: [PATCH] notation in autogui

---
 helm/software/matita/matitaAutoGui.ml | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/helm/software/matita/matitaAutoGui.ml b/helm/software/matita/matitaAutoGui.ml
index 9ba6dd898..c7b06645b 100644
--- a/helm/software/matita/matitaAutoGui.ml
+++ b/helm/software/matita/matitaAutoGui.ml
@@ -35,7 +35,6 @@ let start = ref 0;;
 let len = ref 10;;
 
 let pp c t =
-  (*
   let t = 
     ProofEngineReduction.replace 
       ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false) 
@@ -43,10 +42,6 @@ let pp c t =
   in
     ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
       max_int [] c t
-  *)
-  let names = List.map (function None -> None | Some (x,_) -> Some x) c in
-  let txt_t = CicPp.pp t names in
-  Pcre.replace ~pat:"\\?(\\d+)\\[[^]]*\\]" ~templ:"?<sub>$1</sub>" txt_t
 ;;
 let pp_goal context x = 
   if x == fake_goal then "" else pp context x
-- 
2.39.2