added a call to ppcontext in the case of appl, to ease the localization of the error

[helm.git] / helm / software / components / library / cicElim.ml

diff --git a/helm/software/components/library/cicElim.ml b/helm/software/components/library/cicElim.ml
index c994a9c53865c685bb75ab3ffec85448f0d08db2..3cb5ee4e8bad090f7cc162c23ab32da318148aa4 100644 (file)
--- 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