diff options
author | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
commit | 72b9a7df489ea47b3e5470741fd39f6100d31676 (patch) | |
tree | 60108a573d2a80d2dd4e3833649890e32427ff8d /contrib/funind/functional_principles_proofs.ml | |
parent | 55ce117e8083477593cf1ff2e51a3641c7973830 (diff) |
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'contrib/funind/functional_principles_proofs.ml')
-rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 60 |
1 files changed, 33 insertions, 27 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index ff4f7499..dec7273b 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -621,33 +621,39 @@ let build_proof fun g -> (* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) - match kind_of_term dyn_infos.info with - | Case(_,_,t,_) -> - let g_nb_prod = nb_prod (pf_concl g) in - let type_of_term = pf_type_of g t in - let term_eq = - make_refl_eq type_of_term t + match kind_of_term dyn_infos.info with | Case(ci,ct,t,cb) -> + let do_finalize_t dyn_info' = + fun g -> + let t = dyn_info'.info in + let dyn_infos = {dyn_info' with info = + mkCase(ci,ct,t,cb)} in + let g_nb_prod = nb_prod (pf_concl g) in + let type_of_term = pf_type_of g t in + let term_eq = + make_refl_eq type_of_term t + in + tclTHENSEQ + [ + h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); + thin dyn_infos.rec_hyps; + pattern_option [[-1],t] None; + h_simplest_case t; + (fun g' -> + let g'_nb_prod = nb_prod (pf_concl g') in + let nb_instanciate_partial = g'_nb_prod - g_nb_prod in + observe_tac "treat_new_case" + (treat_new_case + ptes_infos + nb_instanciate_partial + (build_proof do_finalize) + t + dyn_infos) + g' + ) + + ] g in - tclTHENSEQ - [ - h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); - thin dyn_infos.rec_hyps; - pattern_option [[-1],t] None; - h_simplest_case t; - (fun g' -> - let g'_nb_prod = nb_prod (pf_concl g') in - let nb_instanciate_partial = g'_nb_prod - g_nb_prod in - observe_tac "treat_new_case" - (treat_new_case - ptes_infos - nb_instanciate_partial - (build_proof do_finalize) - t - dyn_infos) - g' - ) - - ] g + build_proof do_finalize_t {dyn_infos with info = t} g | Lambda(n,t,b) -> begin match kind_of_term( pf_concl g) with @@ -1474,7 +1480,7 @@ let prove_principle_for_gen (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) ); observe_tac "reverting" (revert (List.rev (acc_rec_arg_id::args_ids))); - observe_tac "h_fix" (h_fix (Some fix_id) (npost_rec_arg + 1)); + observe_tac "h_fix" (h_fix (Some fix_id) (List.length args_ids + 1)); h_intros (List.rev (acc_rec_arg_id::args_ids)); Equality.rewriteLR (mkConst eq_ref); observe_tac "finish" (fun gl' -> |