aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--META.coq4
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--interp/dumpglob.mli4
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/implicit_quantifiers.mli2
-rw-r--r--parsing/extend.ml (renamed from pretyping/extend.ml)0
-rw-r--r--parsing/g_proofs.ml41
-rw-r--r--parsing/parsing.mllib2
-rw-r--r--parsing/vernacexpr.ml (renamed from pretyping/vernacexpr.ml)11
-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/pretyping.mllib2
-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.ml6
21 files changed, 44 insertions, 37 deletions
diff --git a/META.coq b/META.coq
index 3414ccbd4..12d7666cb 100644
--- a/META.coq
+++ b/META.coq
@@ -131,10 +131,10 @@ package "interp" (
package "grammar" (
- description = "Coq Base Grammar"
+ description = "Coq Camlp5 Grammar Extensions for Plugins"
version = "8.8"
- requires = "coq.interp"
+ requires = "camlp5.gramlib"
directory = "grammar"
archive(byte) = "grammar.cma"
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index bc6a1ef3a..74618a290 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -254,7 +254,7 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc ->
let dump_definition {CAst.loc;v=id} sec s =
dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)
-let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty =
+let dump_constraint { CAst.loc; v = n } sec ty =
match n with
| Names.Name id -> dump_definition CAst.(make ?loc id) sec ty
| Names.Anonymous -> ()
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 8dfb4f8f7..bf83d2df4 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -38,8 +38,8 @@ val dump_binding : ?loc:Loc.t -> Names.Id.Set.elt -> unit
val dump_notation :
(Constrexpr.notation * Notation.notation_location) Loc.located ->
Notation_term.scope_name option -> bool -> unit
-val dump_constraint :
- Vernacexpr.typeclass_constraint -> bool -> string -> unit
+
+val dump_constraint : Misctypes.lname -> bool -> string -> unit
val dump_string : string -> unit
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 58df9abc4..289890544 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -58,7 +58,7 @@ let in_generalizable : bool * Misctypes.lident list option -> obj =
classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj)
}
-let declare_generalizable local gen =
+let declare_generalizable ~local gen =
Lib.add_anonymous_leaf (in_generalizable (local, gen))
let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 5f4129ae0..39d0174f9 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -13,7 +13,7 @@ open Glob_term
open Constrexpr
open Libnames
-val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit
+val declare_generalizable : local:bool -> Misctypes.lident list option -> unit
val ids_of_list : Id.t list -> Id.Set.t
val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t
diff --git a/pretyping/extend.ml b/parsing/extend.ml
index 734b859f6..734b859f6 100644
--- a/pretyping/extend.ml
+++ b/parsing/extend.ml
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/parsing/parsing.mllib b/parsing/parsing.mllib
index 1f29636b2..103e1188a 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,5 +1,7 @@
Tok
CLexer
+Extend
+Vernacexpr
Pcoq
Egramml
Egramcoq
diff --git a/pretyping/vernacexpr.ml b/parsing/vernacexpr.ml
index 304a5dadd..6ebf66349 100644
--- a/pretyping/vernacexpr.ml
+++ b/parsing/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 *)
@@ -215,7 +216,7 @@ type syntax_modifier =
type proof_end =
| Admitted
(* name in `Save ident` when closing goal *)
- | Proved of opacity_flag * lident option
+ | Proved of Proof_global.opacity_flag * lident option
type scheme =
| InductionScheme of bool * reference or_by_notation * sort_expr
@@ -350,14 +351,14 @@ type nonrec vernac_expr =
| VernacCoercion of reference or_by_notation *
class_rawexpr * class_rawexpr
| VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr
- | VernacNameSectionHypSet of lident * section_subset_expr
+ | VernacNameSectionHypSet of lident * section_subset_expr
(* Type classes *)
| VernacInstance of
bool * (* abstract instance *)
local_binder_expr list * (* super *)
- typeclass_constraint * (* instance name, class name, params *)
- (bool * constr_expr) option * (* props *)
+ typeclass_constraint * (* instance name, class name, params *)
+ (bool * constr_expr) option * (* props *)
Typeclasses.hint_info_expr
| VernacContext of local_binder_expr list
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/pretyping.mllib b/pretyping/pretyping.mllib
index d98026bc6..c48decdb0 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -27,8 +27,6 @@ Pattern
Patternops
Constr_matching
Tacred
-Extend
-Vernacexpr
Typeclasses_errors
Typeclasses
Classops
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..e1ce4e194 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 =
@@ -855,7 +855,7 @@ let vernac_identity_coercion ~atts id qids qidt =
let vernac_instance ~atts abst sup inst props pri =
let global = not (make_section_locality atts.locality) in
- Dumpglob.dump_constraint inst false "inst";
+ Dumpglob.dump_constraint (fst (pi1 inst)) false "inst";
let program_mode = Flags.is_program_mode () in
ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri)
@@ -1268,7 +1268,7 @@ let vernac_reserve bl =
let vernac_generalizable ~atts =
let local = make_non_locality atts.locality in
- Implicit_quantifiers.declare_generalizable local
+ Implicit_quantifiers.declare_generalizable ~local
let _ =
declare_bool_option
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-14 03:54:36 +0000