X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=d58dc9854bceef447083e2ff628bfe99ef6eee91;hb=58ce236b589513e779e00759e54e72cbbf2bd2c3;hp=dbdb1530f8bd46c6f000b707df82652391633832;hpb=39541174994235283a3c67e0c48b52e067c948af;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index dbdb1530f..d58dc9854 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -345,13 +345,13 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
     | CicNotationPt.LetIn ((name, typ), def, body) ->
         let cic_def = aux ~localize loc context def in
         let cic_name = CicNotationUtil.cic_name_of_name name in
-        let cic_def =
+        let cic_typ =
           match typ with
-          | None -> cic_def
-          | Some t -> Cic.Cast (cic_def, aux ~localize loc context t)
+          | None -> Cic.Implicit (Some `Type)
+          | Some t -> aux ~localize loc context t
         in
         let cic_body = aux ~localize loc (cic_name :: context) body in
-        Cic.LetIn (cic_name, cic_def, cic_body)
+        Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
     | CicNotationPt.LetRec (kind, defs, body) ->
         let context' =
           List.fold_left
@@ -431,9 +431,9 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                Cic.CoFix (n,coinductiveFuns)
         in
          let counter = ref ~-1 in
-         let build_term funs (var,_,_,_) t =
+         let build_term funs (var,_,ty,_) t =
           incr counter;
-          Cic.LetIn (Cic.Name var, fix_or_cofix !counter, t)
+          Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
          in
           (match cic_body with
               `AvoidLetInNoAppl n ->