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
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) =
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
*)
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"