diff options
| author | Gaëtan Gilbert | 2020-07-08 14:06:19 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-08 15:12:46 +0200 |
| commit | 3ef2bd35926a83fbcfd34d03e1fb1db894a39627 (patch) | |
| tree | 5f7bfcaa3f191defa918ff4bcf4e07e1d280f740 /plugins/funind/recdef.ml | |
| parent | 22e2ab01dd9fe4d6b6afb6d1bb171cbf11db4a3f (diff) | |
declare: Add [save_regular] API for obligation-ignoring proofs
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 7b00191026..253c95fa67 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -58,9 +58,8 @@ let declare_fun name kind ?univs value = (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce)) let defined lemma = - let pm = Declare.OblState.empty in - let _pm, _ = - Declare.Proof.save ~pm ~proof:lemma ~opaque:Vernacexpr.Transparent + let (_ : _ list) = + Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None in () @@ -1504,9 +1503,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name [Hints.Hint_db.empty TransparentState.empty false] ])) in let lemma = build_proof env (Evd.from_env env) start_tac end_tac in - let pm = Declare.OblState.empty in - let _pm, _ = - Declare.Proof.save ~pm ~proof:lemma ~opaque:opacity ~idopt:None + let (_ : _ list) = + Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None in () in @@ -1666,9 +1664,8 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref let _ = Flags.silently (fun () -> - let pm = Declare.OblState.empty in - let _pm = - Declare.Proof.save ~pm ~proof:lemma ~opaque:opacity ~idopt:None + let (_ : _ list) = + Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None in ()) () |