+ let _actual_term, iety, _metasenv'', _ugraph =
+ CicRefine.type_of_aux' metasenv' context instantiated_eliminator ugraph
+ in
+ let _actual_meta, actual_args = match iety with
+ | C.Meta (i, _) -> i, []
+ | C.Appl (C.Meta (i, _) :: args) -> i, args
+ | _ -> assert false
+ in
+ (* let _, upto = PEH.split_with_whd (List.nth splits pred_pos) in *)
+ let upto = List.length actual_args in
+ let rec mk_pred metasenv context' pred term' = function
+ | [] -> metasenv, pred, term'
+ | term :: tail ->
+(* FG: we find the predicate for the eliminator as in the rewrite tactic ****)
+ let termty, _ugraph = TC.type_of_aux' metasenv context' term ugraph in
+ let termty = CicReduction.whd context' termty in
+ let fresh_name =
+ FreshNamesGenerator.mk_fresh_name
+ ~subst:[] metasenv context' C.Anonymous ~typ:termty
+ in
+ let hyp = Some (fresh_name, C.Decl 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 ~ugraph ~conjecture:(metano, context, pred) ~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 term' = MS.apply_subst subst term' in
+ let termty = MS.apply_subst subst termty in
+ let pred = PER.replace_with_rel_1_from ~equality:(==) ~what 1 pred in
+ let pred = MS.apply_subst subst pred in
+ let pred = C.Lambda (fresh_name, termty, pred) in
+ mk_pred metasenv (hyp :: context') pred term' tail
+ in
+ let metasenv', pred, term = mk_pred metasenv' context ty term actual_args in
+ HLog.debug ("PRED: " ^ CicPp.ppterm ~metasenv:metasenv' pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv:metasenv') actual_args));
+ upto, metasenv', pred, term
+ in
+(* FG: END OF ADDED PART ****************************************************)
+ let term_to_refine =
+ let f n =
+ if n = pred_pos then pred else
+ if n = 1 then term else C.Implicit None
+ in
+ C.Appl (eliminator_ref :: args_init args_no f)
+ in
+ let refined_term,_refined_termty,metasenv'',_ugraph =
+ CicRefine.type_of_aux' metasenv' context term_to_refine ugraph
+ in
+ let new_goals =
+ ProofEngineHelpers.compare_metasenvs
+ ~oldmetasenv:metasenv ~newmetasenv:metasenv''
+ in
+ let proof' = curi,metasenv'',proofbo,proofty, attrs in
+ let proof'', new_goals' =
+ PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
+ in
+ (* The apply_tactic can have closed some of the new_goals *)
+ let patched_new_goals =
+ let (_,metasenv''',_,_, _) = proof'' in
+ List.filter
+ (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
+ new_goals @ new_goals'
+ in
+ let res = proof'', patched_new_goals in
+ if upto = 0 then res else
+ let continuation = beta_after_elim_tac upto pred in
+ let dummy_status = proof,goal in
+ PET.apply_tactic
+ (T.then_ ~start:(PET.mk_tactic (fun _ -> res)) ~continuation)
+ dummy_status
+ in
+ PET.mk_tactic elim_tac
+;;
+
+let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
+ let cases_tac ~term (proof, goal) =
+ let module TC = CicTypeChecker in
+ let module U = UriManager in
+ let module R = CicReduction in
+ let module C = Cic in
+ let (curi,metasenv,proofbo,proofty, attrs) = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let termty = CicReduction.whd context termty in
+ let (termty,metasenv',arguments,fresh_meta) =
+ TermUtil.saturate_term
+ (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
+ let term = if arguments = [] then term else Cic.Appl (term::arguments) in
+ let uri,exp_named_subst,typeno,args =
+ match termty with
+ | C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
+ | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
+ (uri,exp_named_subst,typeno,args)
+ | _ -> raise NotAnInductiveTypeToEliminate
+ in
+ let paramsno,itty,patterns,right_args =
+ match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ | C.InductiveDefinition (tys,_,paramsno,_),_ ->
+ let _,left_parameters,right_args =
+ List.fold_right
+ (fun x (n,acc1,acc2) ->
+ if n > 0 then (n-1,acc1,x::acc2) else (n,x::acc1,acc2))
+ args (List.length args - paramsno, [],[])
+ in
+ let _,_,itty,cl = List.nth tys typeno in
+ let rec aux left_parameters context t =
+ match left_parameters,CicReduction.whd context t with
+ | [],C.Prod (name,source,target) ->
+ let fresh_name =
+ mk_fresh_name_callback metasenv' context name ~typ:source