X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicParser.ml;h=9fac7badba3a10e0b8eb166df6ca67d88ff31bc0;hb=bb48f187f60642ea1e8db9a73c9ae29042ce02cb;hp=3d1d3d1aa05ccbcd1ee313d8574b870b09fad3bd;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml
index 3d1d3d1aa..9fac7badb 100644
--- a/helm/software/components/cic/cicParser.ml
+++ b/helm/software/components/cic/cicParser.ml
@@ -406,8 +406,15 @@ let end_element ctxt tag =
         | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
         | _ -> attribute_error ())
   | "def" ->  (* same as "decl" above *)
-      let ty = pop_cic ctxt in
-      let source = pop_cic ctxt in
+      let ty,source =
+       (*CSC: hack to parse Coq files where the LetIn is not typed *)
+       let ty = pop_cic ctxt in
+       try
+        let source = pop_cic ctxt in
+         ty,source
+       with
+        Parser_failure _ -> Cic.AImplicit ("MISSING_def_TYPE",None),ty
+      in
       push ctxt
         (match pop_tag_attrs ctxt with
         | ["binder", binder; "id", id]