| C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl)
| C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t)
| C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t)
- | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term k ty, lift_term (succ k) t)
+ | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, lift_term k ty, lift_term k s, lift_term (succ k) t)
| C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl)
| C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl)
in
aux [] c
let elim_inferred_type context goal arg using cpattern =
- let metasenv, ugraph = [], Un.empty_ugraph in
+ let metasenv, ugraph = [], Un.oblivion_ugraph in
let ety, _ugraph = TC.type_of_aux' metasenv context using ugraph in
let _splits, args_no = PEH.split_with_whd (context, ety) in
let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim
let ty = C.Appl (predicate :: actual_args) in
let upto = List.length actual_args in
Rd.head_beta_reduce ~delta:false ~upto ty
+
+let does_not_occur = function
+ | C.AImplicit (_, None) -> true
+ | _ -> false