diff options
| author | Emilio Jesus Gallego Arias | 2019-06-07 15:22:31 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-26 12:27:04 +0200 |
| commit | d4aeb1ef92a9fc35b242a0d91488de60c24d7bbb (patch) | |
| tree | 0c4165866165937fae20b0dfe9a334e55ea3b8b8 /plugins/funind/functional_principles_proofs.ml | |
| parent | 2c39a12f5a8d7178b991595324692c1596ea9199 (diff) | |
[stm] [vernac] Remove special ?proof parameter from vernac main path
We move special vernac-qed handling to a special function, making the
regular vernacular interpretation path uniform.
This is an important step as it paves the way up to export the vernac
DSL to clients, as there are no special vernacs anymore in the regular
interp path, except for Load, which should be handled separately due
to silly reasons, as morally it is a `VtNoProof` command.
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 a904b81d81..f773b2c39e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1005,7 +1005,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num lemma_type in let lemma,_ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in - let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in + let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in evd let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g = |