aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/functional_principles_proofs.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f4fa61a22..91b17b9a4 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1007,7 +1007,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
(mk_equation_id f_id)
(Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem))
evd
- (EConstr.Unsafe.to_constr lemma_type)
+ lemma_type
(Lemmas.mk_hook (fun _ _ -> ()));
ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)));