X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicElim.ml;h=3cb5ee4e8bad090f7cc162c23ab32da318148aa4;hb=aeb225c2bb3291888ce3df279119a8bda4817087;hp=22bece0338e08f7a777a11464cd6ca5adcbaaf8e;hpb=e0142811b372f3c32d34f78dc4ff8ca74b02ef63;p=helm.git

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