From d4aeb1ef92a9fc35b242a0d91488de60c24d7bbb Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 7 Jun 2019 15:22:31 +0200 Subject: [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. --- plugins/funind/recdef.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/funind/recdef.ml') diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 425e498330..b68b31c93b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -71,7 +71,7 @@ let declare_fun f_id kind ?univs value = ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; let defined lemma = - Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None + Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None let def_of_const t = match (Constr.kind t) with @@ -1365,7 +1365,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type ) g) in - Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None + Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None in let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Lemma) @@ -1492,7 +1492,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation } ) )) lemma in - let _ = Flags.silently (fun () -> Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None) () in + let _ = Flags.silently (fun () -> Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None) () in () (* Pp.msgnl (fun _ _ -> str "eqn finished"); *) -- cgit v1.2.3