- let ety,_ =
- T.type_of_aux' metasenv' context eliminator_ref CicUniv.empty_ugraph in
- let rec find_args_no =
- function
- C.Prod (_,_,t) -> 1 + find_args_no t
- | C.Cast (s,_) -> find_args_no s
- | C.LetIn (_,_,t) -> 0 + find_args_no t
- | _ -> 0
- in
- let args_no = find_args_no ety in
- let term_to_refine =
- let rec make_tl base_case =
- function
- 0 -> [base_case]
- | n -> (C.Implicit None)::(make_tl base_case (n - 1))
- in
- C.Appl (eliminator_ref :: make_tl term (args_no - 1))
+ let ety,_ugraph =
+ TC.type_of_aux' metasenv' context eliminator_ref ugraph in
+(* FG: ADDED PART ***********************************************************)
+(* FG: we can not assume eliminator is the default eliminator ***************)
+(*
+ let add_lambdas n t =
+ let rec aux n t =
+ if n <= 0 then t
+ else C.Lambda (C.Anonymous, C.Implicit None, aux (pred n) t)
+ in
+ aux n (S.lift n t)
+ in
+*)
+ let rec args_init n f =
+ if n <= 0 then [] else f n :: args_init (pred n) f
+ in
+ let splits, args_no = PEH.split_with_whd (context, ety) in
+ let pred_pos = match List.hd splits with
+ | _, C.Rel i when i > 1 && i <= args_no -> i
+ | _, C.Appl (C.Rel i :: _) when i > 1 && i <= args_no -> i
+ | _ -> raise NotAnEliminator
+ in
+(*
+ let _, lambdas = PEH.split_with_whd (List.nth splits pred_pos) in
+ let termty_ty =
+ let termty_ty,_ugraph = TC.type_of_aux' metasenv' context termty ugraph in
+ CicReduction.whd context termty_ty
+ 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