X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=34ca16d256e5460fd24f2f00d6b93d60e57abf87;hb=21f1fb39b5e1187ef87387f20522e60abe4f7c19;hp=828002a8bca0a522c484a0b38fd63d2328179e59;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 828002a8b..34ca16d25 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -140,7 +140,11 @@ let wrap_with_make include_paths (f : GrafiteParser.statement) x =
             HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
             assert false
       in
-      if b then f ~include_paths x 
+      if b then 
+        try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ ->
+         raise 
+           (Failure ("Including: "^tgt^
+             "\nNothing to do... did you run matitadep?"))
       else raise (Failure ("Compiling: " ^ tgt))
 ;;
 
@@ -237,13 +241,13 @@ let cic2grafite context menv t =
       | Cic.Prod (Cic.Name n, s, t) ->
           PT.Binder (`Forall, (PT.Ident (n,None), Some (aux c s)),
             aux (Some (Cic.Name n, Cic.Decl s)::c) t)
-      | Cic.LetIn (Cic.Name n, s, t) ->
+      | Cic.LetIn (Cic.Name n, s, ty, t) ->
           PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
-            aux (Some (Cic.Name n, Cic.Def (s,None))::c) t)
+            aux (Some (Cic.Name n, Cic.Def (s,ty))::c) 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
@@ -530,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 
@@ -1111,7 +1115,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