diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 5 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 12 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.mlg | 9 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 11 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 9 | ||||
| -rw-r--r-- | plugins/funind/plugin_base.dune | 1 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
7 files changed, 16 insertions, 33 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 651895aa08..ef1d1af199 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -131,8 +131,7 @@ let finish_proof dynamic_infos g = g -let refine c = - Tacmach.refine c +let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c) let thin l = Proofview.V82.of_tactic (Tactics.clear l) @@ -1487,7 +1486,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = Eauto.eauto_with_bases (true,5) [(fun _ sigma -> (sigma, Lazy.force refl_equal))] - [Hints.Hint_db.empty empty_transparent_state false] + [Hints.Hint_db.empty TransparentState.empty false] ) ) ) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d1e7d8a5a8..1cf952576d 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -320,10 +320,16 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* let dur1 = System.time_difference tim1 tim2 in *) (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) (* end; *) - get_proof_clean true, CEphemeron.create hook - end - + let open Proof_global in + let { id; entries; persistence } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in + match entries with + | [entry] -> + discard_current (); + (id,(entry,persistence)), CEphemeron.create hook + | _ -> + CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") + end let generate_functional_principle (evd: Evd.evar_map ref) interactive_proof diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 155df1c1e0..8f0440a2a4 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -145,7 +145,6 @@ END { -module Gram = Pcoq.Gram module Vernac = Pvernac.Vernac_ module Tactic = Pltac @@ -186,8 +185,8 @@ VERNAC COMMAND EXTEND Function Vernac_classifier.classify_vernac (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with - | Vernacexpr.VtSideff ids, _ when hard -> - Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) + | Vernacextend.VtSideff ids, _ when hard -> + Vernacextend.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) | x -> x } -> { do_generate_principle false (List.map snd recsl) } END @@ -225,7 +224,7 @@ let warning_error names e = VERNAC COMMAND EXTEND NewFunctionalScheme | ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] - => { Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater } + => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } -> { begin @@ -261,7 +260,7 @@ END VERNAC COMMAND EXTEND NewFunctionalCase | ["Functional" "Case" fun_scheme_arg(fas) ] - => { Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater } + => { Vernacextend.(VtSideff[pi1 fas], VtLater) } -> { Functional_principles_types.build_case_scheme fas } END diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index cd2ea3ef88..b68b34ca35 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -147,17 +147,6 @@ let save with_clean id const (locality,_,kind) hook = CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); definition_message id - - -let cook_proof _ = - let (id,(entry,_,strength)) = Pfedit.cook_proof () in - (id,(entry,strength)) - -let get_proof_clean do_reduce = - let result = cook_proof do_reduce in - Proof_global.discard_current (); - result - let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 0c8f40c5cf..c9d153d89f 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -45,15 +45,6 @@ val jmeq_refl : unit -> EConstr.constr val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> Lemmas.declaration_hook CEphemeron.key -> unit -(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and - abort the proof -*) -val get_proof_clean : bool -> - Names.Id.t * - (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind) - - - (* [with_full_print f a] applies [f] to [a] in full printing environment. This function preserves the print settings diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune index 9f583234d8..002eb28eea 100644 --- a/plugins/funind/plugin_base.dune +++ b/plugins/funind/plugin_base.dune @@ -2,5 +2,4 @@ (name recdef_plugin) (public_name coq.plugins.recdef) (synopsis "Coq's functional induction plugin") - (flags :standard -open Gramlib) (libraries coq.plugins.extraction)) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 63a3e0582d..6e5e3f9353 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1359,7 +1359,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp Eauto.eauto_with_bases (true,5) [(fun _ sigma -> (sigma, (Lazy.force refl_equal)))] - [Hints.Hint_db.empty empty_transparent_state false] + [Hints.Hint_db.empty TransparentState.empty false] ] ) ) |