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 ()))
let rec scan_tac ~old_context_length ~index ~tactic =
let scan_tac status =
let (proof, goal) = status in
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let context_length = List.length context in
let rec aux index =
let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
let elim_clear_unfold_tac status =
let (proof, goal) = status in
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let index, ty = PEH.lookup_type metasenv context what in
let tac =
(* 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
- let _, metasenv,_,_, _ = proof in
+ let _, metasenv, _subst, _,_, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in
let old_context_length = List.length context in