diff options
| author | herbelin | 2009-10-03 15:55:11 +0000 |
|---|---|---|
| committer | herbelin | 2009-10-03 15:55:11 +0000 |
| commit | a40e92559339d41eb3a757968de4367d77df712f (patch) | |
| tree | cb0d6f1ac0af6983c10f2663288f73121c141162 /plugins | |
| parent | 60622d207ebbeffb8e0c3d7861858e8ca9819e6e (diff) | |
Fixed small name freshness bug in Functional Scheme ("Heq" name was
not refreshed late enough).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12369 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -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 90eb499422..949150ba54 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -562,14 +562,14 @@ let heq_id = id_of_string "Heq" let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = fun g -> - let heq_id = pf_get_new_id heq_id g in let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in tclTHENLIST [ (* We first introduce the variables *) tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps); (* Then the equation itself *) - introduction_no_check heq_id; + intro_using heq_id; + onLastHypId (fun heq_id -> tclTHENLIST [ (* Then the new hypothesis *) tclMAP introduction_no_check dyn_infos.rec_hyps; (* observe_tac "after_introduction" *)(fun g' -> @@ -599,7 +599,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = } in clean_goal_with_heq ptes_infos continue_tac new_infos g' - ) + )]) ] g |