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/invfun.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/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 587e1fc2e8..86defb2f2f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -815,7 +815,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i))) 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 let finfo = find_Function_infos (fst f_as_constant) in (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) let _,lem_cst_constr = Evd.fresh_global @@ -877,7 +877,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let lemma = fst (Lemmas.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i))) 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 let finfo = find_Function_infos (fst f_as_constant) in let _,lem_cst_constr = Evd.fresh_global (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in |