diff options
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index e5d8fe4c1..0850d556c 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -297,7 +297,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro (hook new_principle_type) ; (* let _tim1 = System.get_time () in *) - Pfedit.by (proof_tac (Array.map mkConst funs) mutr_nparams); + Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams)); (* let _tim2 = System.get_time () in *) (* begin *) (* let dur1 = System.time_difference tim1 tim2 in *) |