From 3c31a89866838b8f2d190cad359836d898eb1b93 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 22 Apr 2008 09:41:34 +0000 Subject: [PATCH] Types for LetIns computed during parsing for Coq objects may contain universes that must be made fresh. --- helm/software/components/cic/deannotate.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) -> -- 2.39.2