diff options
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f773b2c39e..6a5307d8f5 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -992,7 +992,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) let info = Lemmas.Info.make ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in + ~kind:(Decls.(Proof Theorem)) () in let lemma = Lemmas.start_lemma (*i The next call to mk_equation_id is valid since we are constructing the lemma |