let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None
let get_inductive_def uri =
- match E.get_obj Un.empty_ugraph uri with
+ match E.get_obj Un.oblivion_ugraph uri with
| C.InductiveDefinition (tys, _, lpsno, _), _ ->
lpsno, tys
| _ -> assert false
let _, psno = PEH.split_with_whd ([], arity) in
let not_relation = (lpsno = psno) in
let not_recursive = is_not_recursive uri tyno tys in
- let ty_ty, _ = TC.type_of_aux' metasenv context t Un.empty_ugraph in
+ let ty_ty, _ = TC.type_of_aux' metasenv context t Un.oblivion_ugraph in
let sort = match PEH.split_with_whd (context, ty_ty) with
| (_, C.Sort sort) ::_ , _ -> CicPp.ppsort sort
| (_, C.Meta _) :: _, _ -> CicPp.ppsort (C.Type (Un.fresh ()))
(* roba seria ------------------------------------------------------------- *)
-let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort C.CProp])
+let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort (C.CProp (CicUniv.fresh ()))])
?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
let decompose_tac status =
let (proof, goal) = status in