diff options
| author | Pierre-Marie Pédrot | 2020-08-26 11:25:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-26 11:25:10 +0200 |
| commit | a3834f1c1fe6ae24cf28e70c04756b7382028188 (patch) | |
| tree | 97f6ffe3289192a391ab7bbfe5a83926bb0c1005 /plugins/funind/functional_principles_proofs.ml | |
| parent | c222a0d4c5f648e086b02262c4764490e8f231c8 (diff) | |
| parent | 495466d20d53ca33adc69a4d9f6cceb8f30d8aad (diff) | |
Merge PR #12881: Deprecate intro_using
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 743afe4177..72e6006b7e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -483,7 +483,10 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos g = (Proofview.V82.of_tactic (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))) ; (* Then the equation itself *) - Proofview.V82.of_tactic (intro_using heq_id) + Proofview.V82.of_tactic + (intro_using_then heq_id + (* we get the fresh name with onLastHypId *) + (fun _ -> Proofview.tclUNIT ())) ; onLastHypId (fun heq_id -> tclTHENLIST [ (* Then the new hypothesis *) @@ -1113,16 +1116,18 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num in let first_tac : tactic = (* every operations until fix creations *) + (* names are already refreshed *) tclTHENLIST [ observe_tac "introducing params" (Proofview.V82.of_tactic - (intros_using (List.rev_map id_of_decl princ_info.params))) + (intros_mustbe_force (List.rev_map id_of_decl princ_info.params))) ; observe_tac "introducing predictes" (Proofview.V82.of_tactic - (intros_using (List.rev_map id_of_decl princ_info.predicates))) + (intros_mustbe_force + (List.rev_map id_of_decl princ_info.predicates))) ; observe_tac "introducing branches" (Proofview.V82.of_tactic - (intros_using (List.rev_map id_of_decl princ_info.branches))) + (intros_mustbe_force (List.rev_map id_of_decl princ_info.branches))) ; observe_tac "building fixes" mk_fixes ] in let intros_after_fixes : tactic = |