From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 11 Apr 2008 10:33:49 +0000 (+0000)
Subject: when we build the elimination principle we fresh universes to not
X-Git-Tag: make_still_working~5363
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8d2fe36efcace8af46c8b478061c3fa8bb72bc04;p=helm.git

when we build the elimination principle we fresh universes to not
generate tems with different
---

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