From e87288450d4d9e49ac91d179714a73bd0147c0d7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 19 May 2018 16:51:55 +0200 Subject: [api] Move `opacity_flag` to `Proof_global`. `Proof_global` is the main consumer of the flag, which doesn't seem to belong to the AST as plugins show. This will allow the vernac AST to be placed in `vernac` indeed. --- parsing/g_proofs.ml4 | 1 + plugins/derive/derive.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/invfun.ml | 4 ++-- plugins/funind/recdef.ml | 8 ++++---- pretyping/vernacexpr.ml | 3 ++- printing/ppvernac.ml | 1 + proofs/proof_global.ml | 4 +++- proofs/proof_global.mli | 4 +++- stm/stm.ml | 6 +++--- vernac/lemmas.ml | 4 ++-- vernac/obligations.ml | 10 +++++----- vernac/vernacentries.ml | 2 +- 13 files changed, 29 insertions(+), 22 deletions(-) diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index e393c2bbf..4f3d83a8a 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -10,6 +10,7 @@ open Constrexpr open Vernacexpr +open Proof_global open Misctypes open Pcoq diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 8a55538bd..480819ebe 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -61,7 +61,7 @@ let start_deriving f suchthat lemma = | Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> - opaque <> Vernacexpr.Transparent , f_def , lemma_def + opaque <> Proof_global.Transparent , f_def , lemma_def | _ -> assert false in (** The opacity of [f_def] is adjusted to be [false], as it diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 3801fec4b..ccf109ce1 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1013,7 +1013,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num lemma_type (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); - Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))); + Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))); evd diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 180952635..b9d5ebf57 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -818,7 +818,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i)))); - (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))); + (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)))); 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 @@ -879,7 +879,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i)))) ; - (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))); + (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)))); 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 diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2464c595f..45c9eff2f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -72,7 +72,7 @@ let declare_fun f_id kind ?univs value = let ce = definition_entry ?univs value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; -let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None))) +let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Proof_global.Transparent,None))) let def_of_const t = match (Constr.kind t) with @@ -1306,9 +1306,9 @@ let build_new_goal_type () = let is_opaque_constant c = let cb = Global.lookup_constant c in match cb.Declarations.const_body with - | Declarations.OpaqueDef _ -> Vernacexpr.Opaque - | Declarations.Undef _ -> Vernacexpr.Opaque - | Declarations.Def _ -> Vernacexpr.Transparent + | Declarations.OpaqueDef _ -> Proof_global.Opaque + | Declarations.Undef _ -> Proof_global.Opaque + | Declarations.Def _ -> Proof_global.Transparent let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml index 304a5dadd..71a2e8cb8 100644 --- a/pretyping/vernacexpr.ml +++ b/pretyping/vernacexpr.ml @@ -135,7 +135,8 @@ type search_restriction = type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) -type opacity_flag = Opaque | Transparent +type opacity_flag = Proof_global.opacity_flag = Opaque | Transparent + [@ocaml.deprecated "Please use [Proof_global.opacity_flag]"] type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index f26ac0bf9..7a34e8027 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -717,6 +717,7 @@ open Pputils return (keyword "Admitted") | VernacEndProof (Proved (opac,o)) -> return ( + let open Proof_global in match o with | None -> (match opac with | Transparent -> keyword "Defined" diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 97cfccb8d..d5cb5b09f 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -78,9 +78,11 @@ type proof_object = { universes: UState.t; } +type opacity_flag = Opaque | Transparent + type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of Vernacexpr.opacity_flag * + | Proved of opacity_flag * Misctypes.lident option * proof_object diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index bf35fd659..de4cec488 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -48,10 +48,12 @@ type proof_object = { universes: UState.t; } +type opacity_flag = Opaque | Transparent + type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of Vernacexpr.opacity_flag * + | Proved of opacity_flag * Misctypes.lident option * proof_object type proof_terminator diff --git a/stm/stm.ml b/stm/stm.ml index 6b92e4737..b8fe8ddd7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1511,7 +1511,7 @@ end = struct (* {{{ *) stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }) in + expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1661,7 +1661,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }); + expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }); `OK proof end with e -> @@ -2121,7 +2121,7 @@ let collect_proof keep cur hd brkind id = | id :: _ -> Names.Id.to_string id in let loc = (snd cur).loc in let is_defined_expr = function - | VernacEndProof (Proved (Transparent,_)) -> true + | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true | _ -> false in let is_defined = function | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 3d627d2f6..3c7ede3c9 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -334,8 +334,8 @@ let universe_proof_terminator compute_guard hook = Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> let is_opaque, export_seff = match opaque with - | Vernacexpr.Transparent -> false, true - | Vernacexpr.Opaque -> true, false + | Transparent -> false, true + | Opaque -> true, false in let proof = get_proof proof compute_guard (hook (Some (proof.Proof_global.universes))) is_opaque in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1e7721f8f..3bf0ca0a8 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -849,12 +849,12 @@ let obligation_terminator name num guard hook auto pf = let obl = obls.(num) in let status = match obl.obl_status, opq with - | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp () - | (true, _), Vernacexpr.Opaque -> err_not_transp () - | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true - | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> + | (_, Evar_kinds.Expand), Opaque -> err_not_transp () + | (true, _), Opaque -> err_not_transp () + | (false, _), Opaque -> Evar_kinds.Define true + | (_, Evar_kinds.Define true), Transparent -> Evar_kinds.Define false - | (_, status), Vernacexpr.Transparent -> status + | (_, status), Transparent -> status in let obl = { obl with obl_status = false, status } in let ctx = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index eae8167c4..48deea97f 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -518,7 +518,7 @@ let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) let status = Pfedit.by (Tactics.exact_proof c) in - save_proof (Vernacexpr.(Proved(Opaque,None))); + save_proof (Vernacexpr.(Proved(Proof_global.Opaque,None))); if not status then Feedback.feedback Feedback.AddedAxiom let vernac_assumption ~atts discharge kind l nl = -- cgit v1.2.3