X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2Fdeannotate.ml;h=c560af569e031f54a7e37baec625c950fae7d314;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=e81190842c6ff2e09c53e1c7bcc9ac9cb7c87bf8;hpb=44b1f0c3a1e4bdc0abc3b02004c7b385ab63f7c5;p=helm.git

diff --git a/helm/software/components/cic/deannotate.ml b/helm/software/components/cic/deannotate.ml
index e81190842..c560af569 100644
--- a/helm/software/components/cic/deannotate.ml
+++ b/helm/software/components/cic/deannotate.ml
@@ -136,7 +136,7 @@ let rec compute_letin_type context te =
         compute_letin_type ((Some (name,(C.Decl so)))::context) dest)
     | C.LetIn (name,so,C.Implicit _,dest) ->
        let so = compute_letin_type context so in
-       let ty = !type_of_aux' context so in
+       let ty = Unshare.unshare ~fresh_univs:true (!type_of_aux' context so) in
         C.LetIn (name, so, ty,
          compute_letin_type ((Some (name,(C.Def (so,ty))))::context) dest)
     | C.LetIn (name,so,ty,dest) ->