diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c530cbdeac..8e6bbcefdd 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -180,7 +180,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic = [tclTHENLIST [ (* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]); - (* observe_tac "change_hyp_with_using rename " *) (rename_hyp [prov_id,hyp_id]) + (* observe_tac "change_hyp_with_using rename " *) (Proofview.V82.of_tactic (rename_hyp [prov_id,hyp_id])) ]] g exception TOREMOVE @@ -642,7 +642,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = Refiner.tclEVARS evm; Proofview.V82.of_tactic (pose_proof (Name prov_hid) c); thin [hid]; - rename_hyp [prov_hid,hid] + Proofview.V82.of_tactic (rename_hyp [prov_hid,hid]) ] g ) ( (* |