X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicElim.ml;h=3cb5ee4e8bad090f7cc162c23ab32da318148aa4;hb=28a4c3ee256336c0f482235f81b8bd5ad622945a;hp=c994a9c53865c685bb75ab3ffec85448f0d08db2;hpb=95bd260f9bcfd158941fa018fceabc917a77ac96;p=helm.git diff --git a/helm/software/components/library/cicElim.ml b/helm/software/components/library/cicElim.ml index c994a9c53..3cb5ee4e8 100644 --- a/helm/software/components/library/cicElim.ml +++ b/helm/software/components/library/cicElim.ml @@ -217,7 +217,7 @@ let rec branch (uri, typeno) insource paramsno t fix head args = if insource then (match args with | [arg] -> Cic.Appl (fix :: args) - | _ -> Cic.Appl (head :: [Cic.Appl args])) + | _ -> Cic.Appl (fix :: [Cic.Appl args])) else (match args with | [] -> head @@ -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