if b then n else find (n+1) tl
| _ -> find (n+1) tl
)
- | [] -> raise (PET.Fail "Assumption: No such assumption")
+ | [] -> raise (PET.Fail (lazy "Assumption: No such assumption"))
in PET.apply_tactic (PT.apply_tac ~term:(C.Rel (find 1 context))) status
in
PET.mk_tactic assumption_tac
let term =
match term with
None -> None
- | Some term -> Some (CicMetaSubst.apply_subst subst term) in
- let u,typ,term =
- let context_of_t,t =
+ | Some term ->
+ Some (fun context metasenv ugraph ->
+ let term, metasenv, ugraph = term context metasenv ugraph in
+ CicMetaSubst.apply_subst subst term, metasenv, ugraph)
+ in
+ let u,typ,term, metasenv =
+ let context_of_t, (t, metasenv, u) =
match terms_with_context, term with
[], None ->
raise
UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly
- | _, Some t -> context,t
- | (context_of_t,t)::_, None -> context_of_t,t
+ | [], Some t -> context, t context metasenv u
+ | (context_of_t, _)::_, Some t ->
+ context_of_t, t context_of_t metasenv u
+ | (context_of_t, t)::_, None -> context_of_t, (t, metasenv, u)
in
let t,subst,metasenv' =
try
assert (subst = []);
assert (metasenv' = metasenv);
let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in
- u,typ,t
+ u,typ,t,metasenv
in
(* We need to check:
1. whether they live in the context of the goal;