From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 22 Apr 2008 09:41:34 +0000 (+0000)
Subject: Types for LetIns computed during parsing for Coq objects may contain universes
X-Git-Tag: make_still_working~5302
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3c31a89866838b8f2d190cad359836d898eb1b93;p=helm.git

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 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) ->