diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-07 22:44:43 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 10:10:43 +0100 |
| commit | aa99912e9adc566a179b4972ff85a92b967fb134 (patch) | |
| tree | 96a0f2264ce398bd8d6f1a86c5be1fa5aff7391f /plugins/funind/functional_principles_proofs.ml | |
| parent | e8c47b652a0b53f8d3f7eaa877e81910c8de55d0 (diff) | |
Removing redundant versions of generalize.
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 5b9f82aa5..f57f12f66 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -706,7 +706,7 @@ let build_proof in tclTHENSEQ [ - Simple.generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); + generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); thin dyn_infos.rec_hyps; pattern_option [Locus.AllOccurrencesBut [1],t] None; (fun g -> observe_tac "toto" ( @@ -933,7 +933,7 @@ let generalize_non_dep hyp g = in (* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *) tclTHEN - ((* observe_tac "h_generalize" *) (Simple.generalize (List.map mkVar to_revert) )) + ((* observe_tac "h_generalize" *) (generalize (List.map mkVar to_revert) )) ((* observe_tac "thin" *) (thin to_revert)) g @@ -1563,7 +1563,7 @@ let prove_principle_for_gen Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))))) in let revert l = - tclTHEN (Tactics.Simple.generalize (List.map mkVar l)) (clear l) + tclTHEN (Tactics.generalize (List.map mkVar l)) (clear l) in let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in let prove_rec_arg_acc g = |