diff options
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -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 949150ba5..3d789b92e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -968,7 +968,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = ) ] in - Command.start_proof + Lemmas.start_proof (*i The next call to mk_equation_id is valid since we are constructing the lemma Ensures by: obvious i*) @@ -977,7 +977,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = lemma_type (fun _ _ -> ()); Pfedit.by (prove_replacement); - Command.save_named false + Lemmas.save_named false |