aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/g_proofs.ml41
-rw-r--r--plugins/derive/derive.ml2
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/invfun.ml4
-rw-r--r--plugins/funind/recdef.ml8
-rw-r--r--pretyping/vernacexpr.ml3
-rw-r--r--printing/ppvernac.ml1
-rw-r--r--proofs/proof_global.ml4
-rw-r--r--proofs/proof_global.mli4
-rw-r--r--stm/stm.ml6
-rw-r--r--vernac/lemmas.ml4
-rw-r--r--vernac/obligations.ml10
-rw-r--r--vernac/vernacentries.ml2
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 =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 14:41:55 +0000