X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=4fa7d9e5f5389fb0c148de50a5672b2c86c4e5f1;hb=b637879a2b3f2ceda65afb3c950061189c4730b7;hp=ae33d1f83ce4a3d31f391a1ebef36844857c8c07;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index ae33d1f83..4fa7d9e5f 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -247,7 +247,7 @@ let cic2grafite context menv t =
       | Cic.Meta _ -> PT.Implicit
       | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
       | Cic.Sort Cic.Set -> PT.Sort `Set
-      | Cic.Sort Cic.CProp -> PT.Sort `CProp
+      | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
       | Cic.Sort Cic.Prop -> PT.Sort `Prop
       | _ as t -> PT.Ident ("ERROR: "^CicPp.ppterm t, None)
     in
@@ -534,7 +534,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
             Auto.revision time size depth
         in
         let proof_script = 
-          if List.exists (fun (s,_) -> s = "paramodulation") params then
+          if List.exists (fun (s,_) -> s = "paramodulation") (snd params) then
               let proof_term, how_many_lambdas = 
                 Auto.lambda_close ~prefix_name:"orrible_hack_" 
                   proof_term menv cc 
@@ -561,25 +561,11 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
               cic2grafite cc menv proof_term 
             else
               (* alternative using FG stuff *)
-              let proof_term, how_many_lambdas = 
-                Auto.lambda_close ~prefix_name:"orrible_hack_" 
-                  proof_term menv cc 
-              in
-              let ty,_ = 
-                CicTypeChecker.type_of_aux'
-                  menv [] proof_term CicUniv.empty_ugraph
-              in
-              let obj = 
-                Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma])
-              in
-                Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+"
-                 (strip_comments
-                  (ApplyTransformation.txt_of_cic_object
-                    ~map_unicode_to_tex:(Helm_registry.get_bool
-                      "matita.paste_unicode_as_tex")
-                    ~skip_thm_and_qed:true
-                    ~skip_initial_lambdas:how_many_lambdas
-                    80 (GrafiteAst.Procedural None) "" obj)) 
+              let map_unicode_to_tex =
+	         Helm_registry.get_bool "matita.paste_unicode_as_tex"
+	      in
+	      ApplyTransformation.procedural_txt_of_cic_term
+                 ~map_unicode_to_tex 78 cc proof_term
         in
         let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in
         [],text,parsed_text_length
@@ -1115,7 +1101,6 @@ object (self)
           let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in
           (* CSC: why +1 in the following lines ???? *)
           let parsed_text_length = parsed_text_length + 1 in
-prerr_endline ("## " ^ string_of_int parsed_text_length);
           let remain_len = String.length s - parsed_text_length in
           let next = String.sub s parsed_text_length remain_len in
           is_there_only_comments lexicon_status next