From 8d2fe36efcace8af46c8b478061c3fa8bb72bc04 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Apr 2008 10:33:49 +0000 Subject: [PATCH] when we build the elimination principle we fresh universes to not generate tems with different --- helm/software/components/library/cicElim.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/helm/software/components/library/cicElim.ml b/helm/software/components/library/cicElim.ml index 22bece033..3cb5ee4e8 100644 --- a/helm/software/components/library/cicElim.ml +++ b/helm/software/components/library/cicElim.ml @@ -267,6 +267,10 @@ let elim_of ~sort uri typeno = List.nth indTypes typeno with Failure _ -> assert false in + let ty = Unshare.unshare ~fresh_univs:true ty in + let constructors = + List.map (fun (name,c)-> name,Unshare.unshare ~fresh_univs:true c) constructors + in let paramsno = count_pi ty in (* number of (left or right) parameters *) let rightno = paramsno - leftno in let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in -- 2.39.2