Procedural : added some missing cases

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 828002a8bca0a522c484a0b38fd63d2328179e59..ae33d1f83ce4a3d31f391a1ebef36844857c8c07 100644 (file)
--- 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,9 +241,9 @@ 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