Types for LetIns computed during parsing for Coq objects may contain universes

that must be made fresh.

diff --git a/helm/software/components/cic/deannotate.ml b/helm/software/components/cic/deannotate.ml
index e81190842c6ff2e09c53e1c7bcc9ac9cb7c87bf8..c560af569e031f54a7e37baec625c950fae7d314 100644 (file)
--- 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) ->