diff options
| author | Gaëtan Gilbert | 2020-07-09 11:32:41 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-09 11:32:41 +0200 |
| commit | 577ec77f17a872d6bc36073ceeb3cf582fcf01c4 (patch) | |
| tree | 93729a8f221b9d47269279c3672afc2b6854e1ba /plugins/funind | |
| parent | 769823c425f1b3ffc87141ede814976f6cf44128 (diff) | |
| parent | 3ef2bd35926a83fbcfd34d03e1fb1db894a39627 (diff) | |
Merge PR #11836: [obligations] Functionalize Program state
Reviewed-by: SkySkimmer
Ack-by: gares
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 3 | ||||
| -rw-r--r-- | plugins/funind/gen_principle.ml | 10 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 11 |
3 files changed, 15 insertions, 9 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 14d0c04212..743afe4177 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -864,7 +864,8 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma in let (_ : _ list) = - Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None + Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent + ~idopt:None in evd diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index ffce2f8c85..45b1713441 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1526,9 +1526,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) let lemma = fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma in - let (_ : GlobRef.t list) = - Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent - ~idopt:None + let (_ : _ list) = + Declare.Proof.save_regular ~proof:lemma + ~opaque:Vernacexpr.Transparent ~idopt:None in let finfo = match find_Function_infos (fst f_as_constant) with @@ -1599,8 +1599,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) lemma) in let (_ : _ list) = - Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent - ~idopt:None + Declare.Proof.save_regular ~proof:lemma + ~opaque:Vernacexpr.Transparent ~idopt:None in let finfo = match find_Function_infos (fst f_as_constant) with diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 64f62ba1fb..253c95fa67 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -59,7 +59,8 @@ let declare_fun name kind ?univs value = let defined lemma = let (_ : _ list) = - Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None + Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent + ~idopt:None in () @@ -1503,7 +1504,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name in let lemma = build_proof env (Evd.from_env env) start_tac end_tac in let (_ : _ list) = - Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None + Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None in () in @@ -1662,7 +1663,11 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref in let _ = Flags.silently - (fun () -> Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None) + (fun () -> + let (_ : _ list) = + Declare.Proof.save_regular ~proof:lemma ~opaque:opacity ~idopt:None + in + ()) () in () |