X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicElim.ml;h=aacace7b5614e975d718cb7bf8750683f205b7f2;hb=e45ba2323380ad74c296dd4ec16a71be51c069ba;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..aacace7b5 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
@@ -259,7 +259,7 @@ let branch (uri, typeno) insource liftno paramsno t fix head args =
 
 let elim_of ~sort uri typeno =
   counter := ~-1;
-  let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
+  let (obj, univ) = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in
   match obj with
   | Cic.InductiveDefinition (indTypes, params, leftno, _) ->
       let (name, inductive, ty, constructors) =
@@ -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
@@ -390,7 +394,8 @@ debug_print (lazy (CicPp.ppterm eliminator_body));
 *)
       let (computed_type, ugraph) =
         try
-          CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph
+          CicTypeChecker.type_of_aux' [] [] eliminator_body
+          CicUniv.oblivion_ugraph
         with CicTypeChecker.TypeCheckerFailure msg ->
           raise (Elim_failure (lazy (sprintf 
             "type checker failure while type checking:\n%s\nerror:\n%s"