- let fresh_name =
- FreshNamesGenerator.mk_fresh_name
- ~subst:[] metasenv' context C.Anonymous ~typ:termty in
- let lifted_gty = S.lift 1 ty in
- let lifted_conjecture =
- metano, (Some (fresh_name, Cic.Decl ty)) :: context, lifted_gty in
- let lifted_t1 = S.lift 1 t1x in
- let lifted_pattern =
- let lifted_concl_pat =
- match concl_pat with
- | None -> None
- | Some term -> Some (S.lift 1 term) in
- Some (fun c m u ->
- let distance = pred (List.length c - List.length context) in
- S.lift distance lifted_t1, m, u),[],lifted_concl_pat
- in
+ let metasenv', term, pred, upto = match cpatt, termty_ty with
+ | C.Implicit (Some `Hole), _
+ | _, C.Sort C.Prop when lambdas = 0 -> metasenv', term, C.Implicit None, 0
+ | _ ->
+(* FG: we find the predicate for the eliminator as in the rewrite tactic ****)
+ let fresh_name =
+ FreshNamesGenerator.mk_fresh_name
+ ~subst:[] metasenv' context C.Anonymous ~typ:termty
+ in
+ let lazy_term c m u =
+ let distance = List.length c - List.length context in
+ S.lift distance term, m, u
+ in
+ let pattern = Some lazy_term, [], Some cpatt in
+ let subst, metasenv', _ugraph, _conjecture, selected_terms =
+ ProofEngineHelpers.select
+ ~metasenv:metasenv' ~ugraph ~conjecture ~pattern
+ in
+ let metasenv' = MS.apply_subst_metasenv subst metasenv' in
+ let map (_context_of_t, t) l = t :: l in
+ let what = List.fold_right map selected_terms [] in
+ let ty = MS.apply_subst subst ty in
+ let term = MS.apply_subst subst term in
+ let termty = MS.apply_subst subst termty in
+ let abstr_ty = PER.replace_with_rel_1_from ~equality:(==) ~what 1 ty in
+ let abstr_ty = MS.apply_subst subst abstr_ty in
+ let pred_body = C.Lambda (fresh_name, termty, abstr_ty) in
+ metasenv', term, add_lambdas (pred lambdas) pred_body, lambdas
+ in
+(* FG: END OF ADDED PART ****************************************************)