aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/attributes.ml16
-rw-r--r--vernac/attributes.mli6
-rw-r--r--vernac/auto_ind_decl.ml22
-rw-r--r--vernac/class.ml12
-rw-r--r--vernac/classes.ml22
-rw-r--r--vernac/classes.mli14
-rw-r--r--vernac/comAssumption.ml18
-rw-r--r--vernac/comDefinition.ml2
-rw-r--r--vernac/comDefinition.mli14
-rw-r--r--vernac/comFixpoint.ml16
-rw-r--r--vernac/comFixpoint.mli4
-rw-r--r--vernac/declareDef.ml18
-rw-r--r--vernac/declareDef.mli8
-rw-r--r--vernac/indschemes.ml4
-rw-r--r--vernac/lemmas.ml190
-rw-r--r--vernac/lemmas.mli132
-rw-r--r--vernac/locality.ml23
-rw-r--r--vernac/metasyntax.ml94
-rw-r--r--vernac/metasyntax.mli10
-rw-r--r--vernac/obligations.ml41
-rw-r--r--vernac/obligations.mli8
-rw-r--r--vernac/ppvernac.ml2
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/vernacentries.ml225
-rw-r--r--vernac/vernacentries.mli9
-rw-r--r--vernac/vernacextend.ml24
-rw-r--r--vernac/vernacextend.mli17
-rw-r--r--vernac/vernacstate.ml88
-rw-r--r--vernac/vernacstate.mli52
29 files changed, 615 insertions, 478 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 1ad5862d5d..ab14974598 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -73,11 +73,6 @@ module Notations = struct
end
open Notations
-type deprecation = { since : string option ; note : string option }
-
-let mk_deprecation ?(since=None) ?(note=None) () =
- { since ; note }
-
let assert_empty k v =
if v <> VernacFlagEmpty
then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
@@ -213,19 +208,16 @@ let polymorphic =
universe_transform ~warn_unqualified:true >>
qualify_attribute ukey polymorphic_base
-let deprecation_parser : deprecation key_parser = fun orig args ->
+let deprecation_parser : Deprecation.t key_parser = fun orig args ->
assert_once ~name:"deprecation" orig;
match args with
| VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
| VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
- let since = Some since and note = Some note in
- mk_deprecation ~since ~note ()
+ Deprecation.make ~since ~note ()
| VernacFlagList [ "since", VernacFlagLeaf since ] ->
- let since = Some since in
- mk_deprecation ~since ()
+ Deprecation.make ~since ()
| VernacFlagList [ "note", VernacFlagLeaf note ] ->
- let note = Some note in
- mk_deprecation ~note ()
+ Deprecation.make ~note ()
| _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
let deprecation = attribute_of_list ["deprecated",deprecation_parser]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 44688ddafc..53caf49efd 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -43,15 +43,11 @@ end
(** Definitions for some standard attributes. *)
-type deprecation = { since : string option ; note : string option }
-
-val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
-
val polymorphic : bool attribute
val program : bool attribute
val template : bool option attribute
val locality : bool option attribute
-val deprecation : deprecation option attribute
+val deprecation : Deprecation.t option attribute
val canonical : bool attribute
val program_mode_option_name : string list
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 5aec5cac2c..2e84c3275b 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -195,7 +195,7 @@ let build_beq_scheme mode kn =
let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in
let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in
match Constr.kind c with
- | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants
+ | Rel x -> mkRel (x-nlist+ndx), Evd.empty_side_effects
| Var x ->
(* Support for working in a context with "eq_x : x -> x -> bool" *)
let eid = Id.of_string ("eq_"^(Id.to_string x)) in
@@ -203,11 +203,11 @@ let build_beq_scheme mode kn =
try ignore (Environ.lookup_named eid env)
with Not_found -> raise (ParameterWithoutEquality (VarRef x))
in
- mkVar eid, Safe_typing.empty_private_constants
+ mkVar eid, Evd.empty_side_effects
| Cast (x,_,_) -> aux (Term.applist (x,a))
| App _ -> assert false
| Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
- if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
+ if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Evd.empty_side_effects
else begin
try
let eq, eff =
@@ -216,7 +216,7 @@ let build_beq_scheme mode kn =
let eqa, eff =
let eqa, effs = List.split (List.map aux a) in
Array.of_list eqa,
- List.fold_left Safe_typing.concat_private eff (List.rev effs)
+ List.fold_left Evd.concat_side_effects eff (List.rev effs)
in
let args =
Array.append
@@ -239,7 +239,7 @@ let build_beq_scheme mode kn =
let kneq = Constant.change_label kn eq_lbl in
try let _ = Environ.constant_opt_value_in env (kneq, u) in
Term.applist (mkConst kneq,a),
- Safe_typing.empty_private_constants
+ Evd.empty_side_effects
with Not_found -> raise (ParameterWithoutEquality (ConstRef kn)))
| Proj _ -> raise (EqUnknown "projection")
| Construct _ -> raise (EqUnknown "constructor")
@@ -270,7 +270,7 @@ let build_beq_scheme mode kn =
let constrsi = constrs (3+nparrec) in
let n = Array.length constrsi in
let ar = Array.make n (ff ()) in
- let eff = ref Safe_typing.empty_private_constants in
+ let eff = ref Evd.empty_side_effects in
for i=0 to n-1 do
let nb_cstr_args = List.length constrsi.(i).cs_args in
let ar2 = Array.make n (ff ()) in
@@ -288,7 +288,7 @@ let build_beq_scheme mode kn =
(nb_cstr_args+ndx+1)
cc
in
- eff := Safe_typing.concat_private eff' !eff;
+ eff := Evd.concat_side_effects eff' !eff;
Array.set eqs ndx
(mkApp (eqA,
[|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|]
@@ -320,7 +320,7 @@ let build_beq_scheme mode kn =
let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
types = Array.make nb_ind mkSet and
cores = Array.make nb_ind mkSet in
- let eff = ref Safe_typing.empty_private_constants in
+ let eff = ref Evd.empty_side_effects in
let u = Univ.Instance.empty in
for i=0 to (nb_ind-1) do
names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant;
@@ -328,7 +328,7 @@ let build_beq_scheme mode kn =
(mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ()));
let c, eff' = make_one_eq i in
cores.(i) <- c;
- eff := Safe_typing.concat_private eff' !eff
+ eff := Evd.concat_side_effects eff' !eff
done;
(Array.init nb_ind (fun i ->
let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in
@@ -938,7 +938,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
Not_found ->
Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.")
end >>= fun (lbI,eff'') ->
- let eff = (Safe_typing.concat_private eff'' (Safe_typing.concat_private eff' eff)) in
+ let eff = (Evd.concat_side_effects eff'' (Evd.concat_side_effects eff' eff)) in
Tacticals.New.tclTHENLIST [
Proofview.tclEFFECTS eff;
intros_using fresh_first_intros;
@@ -1005,7 +1005,7 @@ let make_eq_decidability mode mind =
(EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec))
(compute_dec_tact ind lnamesparrec nparrec)
in
- ([|ans|], ctx), Safe_typing.empty_private_constants
+ ([|ans|], ctx), Evd.empty_side_effects
let eq_dec_scheme_kind =
declare_mutual_scheme_object "_eq_dec" make_eq_decidability
diff --git a/vernac/class.ml b/vernac/class.ml
index f3a279eab1..58cef5db4f 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -358,9 +358,9 @@ let try_add_new_coercion_with_source ref ~local poly ~source =
let add_coercion_hook poly _uctx _trans local ref =
let local = match local with
- | Discharge
- | Local -> true
- | Global -> false
+ | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *)
+ | Global ImportNeedQualified -> true
+ | Global ImportDefaultBehavior -> false
in
let () = try_add_new_coercion ref ~local poly in
let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
@@ -370,9 +370,9 @@ let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
let add_subclass_hook poly _uctx _trans local ref =
let stre = match local with
- | Local -> true
- | Global -> false
- | Discharge -> assert false
+ | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *)
+ | Global ImportNeedQualified -> true
+ | Global ImportDefaultBehavior -> false
in
let cl = class_of_global ref in
try_add_new_coercion_subclass cl ~local:stre poly
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 9cc8467c57..b64af52b6e 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -367,7 +367,7 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt
let hook = Lemmas.mk_hook hook in
let ctx = Evd.evar_universe_context sigma in
ignore(Obligations.add_definition id ?term:constr
- ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls)
+ ~univdecl:decl typ ctx ~kind:(Global ImportDefaultBehavior,poly,Instance) ~hook obls)
let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids term termtype =
@@ -377,12 +377,12 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te
the refinement manually.*)
let gls = List.rev (Evd.future_goals sigma) in
let sigma = Evd.reset_future_goals sigma in
- let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
- let pstate = Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
+ let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in
+ let lemma = Lemmas.start_lemma id ~pl:decl kind sigma (EConstr.of_constr termtype)
~hook:(Lemmas.mk_hook
(fun _ _ _ -> instance_hook pri global imps ?hook)) in
(* spiwack: I don't know what to do with the status here. *)
- let pstate =
+ let lemma =
if not (Option.is_empty term) then
let init_refine =
Tacticals.New.tclTHENLIST [
@@ -391,18 +391,18 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te
Tactics.New.reduce_after_refine;
]
in
- let pstate, _ = Pfedit.by init_refine pstate in
- pstate
+ let lemma, _ = Lemmas.by init_refine lemma in
+ lemma
else
- let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in
- pstate
+ let lemma, _ = Lemmas.by (Tactics.auto_intros_tac ids) lemma in
+ lemma
in
match tac with
| Some tac ->
- let pstate, _ = Pfedit.by tac pstate in
- pstate
+ let lemma, _ = Lemmas.by tac lemma in
+ lemma
| None ->
- pstate
+ lemma
let do_instance_subst_constructor_and_ty subst k u ctx =
let subst =
diff --git a/vernac/classes.mli b/vernac/classes.mli
index e61935c87a..ace9096469 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -31,8 +31,8 @@ val declare_instance : ?warn:bool -> env -> Evd.evar_map ->
val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
(** globality, reference, optional priority and pattern information *)
-val new_instance_interactive :
- ?global:bool (** Not global by default. *)
+val new_instance_interactive
+ : ?global:bool (** Not global by default. *)
-> Decl_kinds.polymorphic
-> name_decl
-> local_binder_expr list
@@ -41,10 +41,10 @@ val new_instance_interactive :
-> ?tac:unit Proofview.tactic
-> ?hook:(GlobRef.t -> unit)
-> Hints.hint_info_expr
- -> Id.t * Proof_global.t
+ -> Id.t * Lemmas.t
-val new_instance :
- ?global:bool (** Not global by default. *)
+val new_instance
+ : ?global:bool (** Not global by default. *)
-> Decl_kinds.polymorphic
-> name_decl
-> local_binder_expr list
@@ -55,8 +55,8 @@ val new_instance :
-> Hints.hint_info_expr
-> Id.t
-val new_instance_program :
- ?global:bool (** Not global by default. *)
+val new_instance_program
+ : ?global:bool (** Not global by default. *)
-> Decl_kinds.polymorphic
-> name_decl
-> local_binder_expr list
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index c37e90650a..591e4b130f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -37,15 +37,15 @@ let () =
optwrite = (:=) axiom_into_instance; }
let should_axiom_into_instance = function
- | Discharge ->
+ | Context ->
(* The typeclass behaviour of Variable and Context doesn't depend
on section status *)
true
- | Global | Local -> !axiom_into_instance
+ | Definitional | Logical | Conjectural -> !axiom_into_instance
let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
match local with
-| Discharge when Lib.sections_are_opened () ->
+| Discharge ->
let ctx = match ctx with
| Monomorphic_entry ctx -> ctx
| Polymorphic_entry (_, ctx) -> Univ.ContextSet.of_context ctx
@@ -61,9 +61,8 @@ match local with
let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
(r,Univ.Instance.empty,true)
-| Global | Local | Discharge ->
- let do_instance = should_axiom_into_instance local in
- let local = DeclareDef.get_locality ident ~kind:"axiom" local in
+| Global local ->
+ let do_instance = should_axiom_into_instance kind in
let inl = let open Declaremods in match nl with
| NoInline -> None
| DefaultInline -> Some (Flags.get_inline_level())
@@ -78,6 +77,7 @@ match local with
let env = Global.env () in
let sigma = Evd.from_env env in
let () = if do_instance then Classes.declare_instance env sigma None false gr in
+ let local = match local with ImportNeedQualified -> true | ImportDefaultBehavior -> false in
let () = if is_coe then Class.try_add_new_coercion gr ~local p in
let inst = match ctx with
| Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
@@ -124,7 +124,7 @@ let process_assumptions_udecls kind l =
| (_, ([], _))::_ | [] -> assert false
in
let () = match kind, udecl with
- | (Discharge, _, _), Some _ when Lib.sections_are_opened () ->
+ | (Discharge, _, _), Some _ ->
let loc = first_id.CAst.loc in
let msg = Pp.str "Section variables cannot be polymorphic." in
user_err ?loc msg
@@ -288,7 +288,9 @@ let context poly l =
| _ -> false
in
let impl = List.exists test impls in
- let decl = (Discharge, poly, Definitional) in
+ let persistence =
+ if Lib.sections_are_opened () then Discharge else Global ImportDefaultBehavior in
+ let decl = (persistence, poly, Context) in
let nstatus = match b with
| None ->
pi3 (declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 4cae4b8a74..1046e354a7 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -86,7 +86,7 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
if program_mode then
let env = Global.env () in
let (c,ctx), sideff = Future.force ce.const_entry_body in
- assert(Safe_typing.empty_private_constants = sideff);
+ assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
assert(Univ.ContextSet.is_empty ctx);
Obligations.check_evars env evd;
let c = EConstr.of_constr c in
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index fa4860b079..0d9df47ee8 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -33,7 +33,13 @@ val do_definition
(************************************************************************)
(** Not used anywhere. *)
-val interp_definition : program_mode:bool ->
- universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
- constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
- UState.universe_decl * Impargs.manual_implicits
+val interp_definition
+ : program_mode:bool
+ -> universe_decl_expr option
+ -> local_binder_expr list
+ -> polymorphic
+ -> red_expr option
+ -> constr_expr
+ -> constr_expr option
+ -> Evd.side_effects definition_entry *
+ Evd.evar_map * UState.universe_decl * Impargs.manual_implicits
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 7a4e6d8698..6068cd90f1 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -267,10 +267,10 @@ let declare_fixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),p
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
fixdefs) in
let evd = Evd.from_ctx ctx in
- let pstate = Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint)
+ let lemma = Lemmas.start_lemma_with_initialization (local,poly,DefinitionBody Fixpoint)
evd pl (Some(false,indexes,init_tac)) thms None in
declare_fixpoint_notations ntns;
- pstate
+ lemma
let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
(* We shortcut the proof process *)
@@ -286,7 +286,8 @@ let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximp
let evd = Evd.restrict_universe_context evd vars in
let ctx = Evd.check_univ_decl ~poly evd pl in
let pl = Evd.universe_binders evd in
- let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
+ let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in
+ let fixdecls = List.map mk_pure fixdecls in
ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
@@ -304,11 +305,11 @@ let declare_cofixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes)
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
fixdefs) in
let evd = Evd.from_ctx ctx in
- let pstate = Lemmas.start_proof_with_initialization
- (Global,poly, DefinitionBody CoFixpoint)
+ let lemma = Lemmas.start_lemma_with_initialization
+ (Global ImportDefaultBehavior,poly, DefinitionBody CoFixpoint)
evd pl (Some(true,[],init_tac)) thms None in
declare_cofixpoint_notations ntns;
- pstate
+ lemma
let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
(* We shortcut the proof process *)
@@ -316,7 +317,8 @@ let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fixi
let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
let vars = Vars.universes_of_constr (List.hd fixdecls) in
- let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
+ let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in
+ let fixdecls = List.map mk_pure fixdecls in
let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
let evd = Evd.from_ctx ctx in
let evd = Evd.restrict_universe_context evd vars in
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index c8d617da5f..a31f3c34e0 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -19,13 +19,13 @@ open Vernacexpr
(** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
val do_fixpoint_interactive :
- locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t
+ locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Lemmas.t
val do_fixpoint :
locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
val do_cofixpoint_interactive :
- locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t
+ locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t
val do_cofixpoint :
locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index bdda3314ca..652dbf0858 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -14,27 +14,13 @@ open Entries
open Globnames
open Impargs
-let warn_local_declaration =
- CWarnings.create ~name:"local-declaration" ~category:"scope"
- Pp.(fun (id,kind) ->
- Names.Id.print id ++ strbrk " is declared as a local " ++ str kind)
-
-let get_locality id ~kind = function
-| Discharge ->
- (* If a Let is defined outside a section, then we consider it as a local definition *)
- warn_local_declaration (id,kind);
- true
-| Local -> true
-| Global -> false
-
let declare_definition ident (local, p, k) ?hook_data ce pl imps =
let fix_exn = Future.fix_exn_of ce.const_entry_body in
let gr = match local with
- | Discharge when Lib.sections_are_opened () ->
+ | Discharge ->
let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in
VarRef ident
- | Discharge | Local | Global ->
- let local = get_locality ident ~kind:"definition" local in
+ | Global local ->
let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
let gr = ConstRef kn in
let () = Declare.declare_univ_binders gr pl in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index c4500d0a6b..909aa41a30 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -11,13 +11,11 @@
open Names
open Decl_kinds
-val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
-
val declare_definition
: Id.t
-> definition_kind
-> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
- -> Safe_typing.private_constants Entries.definition_entry
+ -> Evd.side_effects Entries.definition_entry
-> UnivNames.universe_binders
-> Impargs.manual_implicits
-> GlobRef.t
@@ -29,7 +27,7 @@ val declare_fix
-> UnivNames.universe_binders
-> Entries.universes_entry
-> Id.t
- -> Safe_typing.private_constants Entries.proof_output
+ -> Evd.side_effects Entries.proof_output
-> Constr.types
-> Impargs.manual_implicits
-> GlobRef.t
@@ -38,7 +36,7 @@ val prepare_definition : allow_evars:bool ->
?opaque:bool -> ?inline:bool -> poly:bool ->
Evd.evar_map -> UState.universe_decl ->
types:EConstr.t option -> body:EConstr.t ->
- Evd.evar_map * Safe_typing.private_constants Entries.definition_entry
+ Evd.evar_map * Evd.side_effects Entries.definition_entry
val prepare_parameter : allow_evars:bool ->
poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types ->
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index de7d2fd49a..f18cf17bf9 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -414,7 +414,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
let declare decl fi lrecref =
let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
let decltype = EConstr.to_constr sigma decltype in
- let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+ let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in
let cst = define ~poly fi UserIndividualRequest sigma proof_output (Some decltype) in
ConstRef cst :: lrecref
in
@@ -536,7 +536,7 @@ let do_combined_scheme name schemes =
schemes
in
let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
- let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+ let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Evd.empty_side_effects) in
(* It is possible for the constants to have different universe
polymorphism from each other, however that is only when the user
manually defined at least one of them (as Scheme would pick the
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d14c7ddf8f..a7366b2c56 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -26,7 +26,6 @@ open Decl_kinds
open Declare
open Pretyping
open Termops
-open Namegen
open Reductionops
open Constrintern
open Impargs
@@ -46,6 +45,44 @@ let call_hook ?hook ?fix_exn uctx trans l c =
let e = Option.cata (fun fix -> fix e) e fix_exn in
iraise e
+(* Support for terminators and proofs with an associated constant
+ [that can be saved] *)
+
+type proof_ending =
+ | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
+ | Proved of Proof_global.opacity_flag *
+ lident option *
+ Proof_global.proof_object
+
+type proof_terminator = (proof_ending -> unit) CEphemeron.key
+
+(* Proofs with a save constant function *)
+type t =
+ { proof : Proof_global.t
+ ; terminator : proof_terminator
+ }
+
+let pf_map f { proof; terminator} = { proof = f proof; terminator }
+let pf_fold f ps = f ps.proof
+
+let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t)
+
+(* To be removed *)
+module Internal = struct
+
+let make_terminator f = CEphemeron.create f
+let apply_terminator f = CEphemeron.get f
+
+(** Gets the current terminator without checking that the proof has
+ been completed. Useful for the likes of [Admitted]. *)
+let get_terminator ps = ps.terminator
+
+end
+
+let by tac { proof; terminator } =
+ let proof, res = Pfedit.by tac proof in
+ { proof; terminator}, res
+
(* Support for mutually proved theorems *)
let retrieve_first_recthm uctx = function
@@ -75,7 +112,7 @@ let adjust_guardness_conditions const = function
List.interval 0 (List.length ((lam_assum c))))
lemma_guard (Array.to_list fixdefs) in
*)
- let env = Safe_typing.push_private_constants env eff in
+ let env = Safe_typing.push_private_constants env eff.Evd.seff_private in
let indexes =
search_guard env
possible_indexes fixdecls in
@@ -178,18 +215,14 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes
let k = Kindops.logical_kind_of_goal_kind kind in
let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in
let r = match locality with
- | Discharge when Lib.sections_are_opened () ->
+ | Discharge ->
let c = SectionLocalDef const in
let _ = declare_variable id (Lib.cwd(), c, k) in
let () = if should_suggest
then Proof_using.suggest_variable (Global.env ()) id
in
VarRef id
- | Local | Global | Discharge ->
- let local = match locality with
- | Local | Discharge -> true
- | Global -> false
- in
+ | Global local ->
let kn =
declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
let () = if should_suggest
@@ -207,13 +240,10 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes
let default_thm_id = Id.of_string "Unnamed_thm"
-let fresh_name_for_anonymous_theorem () =
- next_global_ident_away default_thm_id Id.Set.empty
-
let check_name_freshness locality {CAst.loc;v=id} : unit =
(* We check existence here: it's a bit late at Qed time *)
if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
- locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
+ locality <> Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
then
user_err ?loc (Id.print id ++ str " already exists.")
@@ -233,16 +263,12 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i
in
let c = SectionLocalAssum ((t_i, univs),p,impl) in
let _ = declare_variable id (Lib.cwd(),c,k) in
- (Discharge, VarRef id,imps)
- | Local | Global ->
- let local = match locality with
- | Local -> true
- | Global -> false
- | Discharge -> assert false
- in
+ (VarRef id,imps)
+ | Global local ->
+ let k = IsAssumption Conjectural in
let decl = (ParameterEntry (None,(t_i,univs),None), k) in
let kn = declare_constant id ~local decl in
- (locality,ConstRef kn,imps))
+ (ConstRef kn,imps))
| Some body ->
let body = norm body in
let k = Kindops.logical_kind_of_goal_kind kind in
@@ -260,45 +286,39 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i
let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
let c = SectionLocalDef const in
let _ = declare_variable id (Lib.cwd(), c, k) in
- (Discharge,VarRef id,imps)
- | Local | Global ->
- let local = match locality with
- | Local -> true
- | Global -> false
- | Discharge -> assert false
- in
+ (VarRef id,imps)
+ | Global local ->
let const =
Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i
in
let kn = declare_constant id ~local (DefinitionEntry const, k) in
- (locality,ConstRef kn,imps)
+ (ConstRef kn,imps)
let check_anonymity id save_ident =
if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
user_err Pp.(str "This command can only be used for unnamed theorem.")
(* Admitted *)
-
let warn_let_as_axiom =
CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
(fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++
- spc () ++ strbrk "declared as an axiom.")
+ spc () ++ strbrk "declared as a local axiom.")
let admit ?hook ctx (id,k,e) pl () =
- let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
- let () = match k with
- | Global, _, _ -> ()
- | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
+ let local = match k with
+ | Global local, _, _ -> local
+ | Discharge, _, _ -> warn_let_as_axiom id; ImportNeedQualified
in
+ let kn = declare_constant id ~local (ParameterEntry e, IsAssumption Conjectural) in
let () = assumption_message id in
Declare.declare_univ_binders (ConstRef kn) pl;
- call_hook ?hook ctx [] Global (ConstRef kn)
+ call_hook ?hook ctx [] (Global local) (ConstRef kn)
(* Starting a goal *)
let standard_proof_terminator ?(hook : declaration_hook option) compute_guard =
let open Proof_global in
- make_terminator begin function
+ CEphemeron.create begin function
| Admitted (id,k,pe,ctx) ->
let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in
Feedback.feedback Feedback.AddedAxiom
@@ -325,7 +345,41 @@ let initialize_named_context_for_proof () =
let d = if variable_opacity id then NamedDecl.drop_body d else d in
Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
-let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
+module Stack = struct
+
+ type lemma = t
+ type nonrec t = t * t list
+
+ let map f (pf, pfl) = (f pf, List.map f pfl)
+
+ let map_top ~f (pf, pfl) = (f pf, pfl)
+ let map_top_pstate ~f (pf, pfl) = (pf_map f pf, pfl)
+
+ let pop (ps, p) = match p with
+ | [] -> ps, None
+ | pp :: p -> ps, Some (pp, p)
+
+ let with_top (p, _) ~f = f p
+ let with_top_pstate (p, _) ~f = f p.proof
+
+ let push ontop a =
+ match ontop with
+ | None -> a , []
+ | Some (l,ls) -> a, (l :: ls)
+
+ let get_all_proof_names (pf : t) =
+ let prj x = Proof_global.get_proof x in
+ let (pn, pns) = map Proof.(function pf -> (data (prj pf.proof)).name) pf in
+ pn :: pns
+
+ let copy_terminators ~src ~tgt =
+ let (ps, psl), (ts,tsl) = src, tgt in
+ assert(List.length psl = List.length tsl);
+ {ts with terminator = ps.terminator}, List.map2 (fun op p -> { p with terminator = op.terminator }) psl tsl
+
+end
+
+let start_lemma id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
let terminator = match terminator with
| None -> standard_proof_terminator ?hook compute_guard
| Some terminator -> terminator ?hook compute_guard
@@ -336,7 +390,16 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
| None -> initialize_named_context_for_proof ()
in
let goals = [ Global.env_of_context sign , c ] in
- Proof_global.start_proof sigma id ?pl kind goals terminator
+ let proof = Proof_global.start_proof sigma id ?pl kind goals in
+ { proof ; terminator }
+
+let start_dependent_lemma id ?pl kind ?terminator ?sign ?(compute_guard=[]) ?hook telescope =
+ let terminator = match terminator with
+ | None -> standard_proof_terminator ?hook compute_guard
+ | Some terminator -> terminator ?hook compute_guard
+ in
+ let proof = Proof_global.start_dependent_proof id ?pl kind telescope in
+ { proof ; terminator }
let rec_tac_initializer finite guard thms snl =
if finite then
@@ -352,7 +415,7 @@ let rec_tac_initializer finite guard thms snl =
| (id,n,_)::l -> Tactics.mutual_fix id n l 0
| _ -> assert false
-let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
+let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in
let init_tac,guard = match recguard with
| Some (finite,guard,init_tac) ->
@@ -380,18 +443,18 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
let env = Global.env () in
List.map_i (save_remaining_recthms env sigma kind norm uctx body opaq) 1 other_thms in
- let thms_data = (strength,ref,imps)::other_thms_data in
- List.iter (fun (strength,ref,imps) ->
+ let thms_data = (ref,imps)::other_thms_data in
+ List.iter (fun (ref,imps) ->
maybe_declare_manual_implicits false ref imps;
call_hook ?hook ctx [] strength ref) thms_data in
- let pstate = start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
- let pstate = Proof_global.modify_proof (fun p ->
+ let lemma = start_lemma id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
+ let lemma = pf_map (Proof_global.map_proof (fun p ->
match init_tac with
| None -> p
- | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in
- pstate
+ | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma in
+ lemma
-let start_proof_com ~program_mode ?inference_hook ?hook kind thms =
+let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
let env0 = Global.env () in
let decl = fst (List.hd thms) in
let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
@@ -423,7 +486,7 @@ let start_proof_com ~program_mode ?inference_hook ?hook kind thms =
else (* We fix the variables to ensure they won't be lowered to Set *)
Evd.fix_undefined_variables evd
in
- start_proof_with_initialization ?hook kind evd decl recguard thms snl
+ start_lemma_with_initialization ?hook kind evd decl recguard thms snl
(* Saving a proof *)
@@ -438,7 +501,7 @@ let () =
optread = (fun () -> !keep_admitted_vars);
optwrite = (fun b -> keep_admitted_vars := b) }
-let save_proof_admitted ?proof ~pstate =
+let save_lemma_admitted ?proof ~(lemma : t) =
let pe =
let open Proof_global in
match proof with
@@ -453,8 +516,8 @@ let save_proof_admitted ?proof ~pstate =
let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
| None ->
- let pftree = Proof_global.give_me_the_proof pstate in
- let gk = Proof_global.get_current_persistence pstate in
+ let pftree = Proof_global.get_proof lemma.proof in
+ let gk = Proof_global.get_persistence lemma.proof in
let Proof.{ name; poly; entry } = Proof.data pftree in
let typ = match Proofview.initial_goals entry with
| [typ] -> snd typ
@@ -466,10 +529,10 @@ let save_proof_admitted ?proof ~pstate =
let universes = Proof.((data pftree).initial_euctx) in
(* This will warn if the proof is complete *)
let pproofs, _univs =
- Proof_global.return_proof ~allow_partial:true pstate in
+ Proof_global.return_proof ~allow_partial:true lemma.proof in
let sec_vars =
if not !keep_admitted_vars then None
- else match Proof_global.get_used_variables pstate, pproofs with
+ else match Proof_global.get_used_variables lemma.proof, pproofs with
| Some _ as x, _ -> x
| None, (pproof, _) :: _ ->
let env = Global.env () in
@@ -477,32 +540,23 @@ let save_proof_admitted ?proof ~pstate =
let ids_def = Environ.global_vars_set env pproof in
Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
| _ -> None in
- let decl = Proof_global.get_universe_decl pstate in
+ let decl = Proof_global.get_universe_decl lemma.proof in
let ctx = UState.check_univ_decl ~poly universes decl in
Admitted(name,gk,(sec_vars, (typ, ctx), None), universes)
in
- Proof_global.apply_terminator (Proof_global.get_terminator pstate) pe
-
-let save_pstate_proved ~pstate ~opaque ~idopt =
- let obj, terminator = Proof_global.close_proof ~opaque
- ~keep_body_ucst_separate:false (fun x -> x) pstate
- in
- Proof_global.(apply_terminator terminator (Proved (opaque, idopt, obj)))
+ CEphemeron.get lemma.terminator pe
-let save_proof_proved ?proof ?ontop ~opaque ~idopt =
+let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
(* Invariant (uh) *)
- if Option.is_empty ontop && Option.is_empty proof then
+ if Option.is_empty lemma && Option.is_empty proof then
user_err (str "No focused proof (No proof-editing in progress).");
let (proof_obj,terminator) =
match proof with
| None ->
(* XXX: The close_proof and proof state API should be refactored
so it is possible to insert proofs properly into the state *)
- let pstate = Proof_global.get_current_pstate @@ Option.get ontop in
- Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pstate
+ let { proof; terminator } = Option.get lemma in
+ Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, terminator
| Some proof -> proof
in
- (* if the proof is given explicitly, nothing has to be deleted *)
- let ontop = if Option.is_empty proof then Proof_global.discard_current Option.(get ontop) else ontop in
- Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj)));
- ontop
+ CEphemeron.get terminator (Proved (opaque,idopt,proof_obj))
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 3df543156d..ac647af8b5 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -11,6 +11,7 @@
open Names
open Decl_kinds
+(* Declaration hooks *)
type declaration_hook
(* Hooks allow users of the API to perform arbitrary actions at
@@ -37,53 +38,120 @@ val call_hook
-> ?fix_exn:Future.fix_exn
-> hook_type
-val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
- ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
- ?sign:Environ.named_context_val ->
- ?compute_guard:Proof_global.lemma_possible_guards ->
- ?hook:declaration_hook -> EConstr.types -> Proof_global.t
+(* Proofs that define a constant + terminators *)
+type t
+type proof_terminator
-val start_proof_com
+module Stack : sig
+
+ type lemma = t
+ type t
+
+ val pop : t -> lemma * t option
+ val push : t option -> lemma -> t
+
+ val map_top : f:(lemma -> lemma) -> t -> t
+ val map_top_pstate : f:(Proof_global.t -> Proof_global.t) -> t -> t
+
+ val with_top : t -> f:(lemma -> 'a ) -> 'a
+ val with_top_pstate : t -> f:(Proof_global.t -> 'a ) -> 'a
+
+ val get_all_proof_names : t -> Names.Id.t list
+
+ val copy_terminators : src:t -> tgt:t -> t
+ (** Gets the current terminator without checking that the proof has
+ been completed. Useful for the likes of [Admitted]. *)
+
+end
+
+val standard_proof_terminator
+ : ?hook:declaration_hook
+ -> Proof_global.lemma_possible_guards
+ -> proof_terminator
+
+val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
+val pf_map : (Proof_global.t -> Proof_global.t) -> t -> t
+val pf_fold : (Proof_global.t -> 'a) -> t -> 'a
+
+val by : unit Proofview.tactic -> t -> t * bool
+
+(* Start of high-level proofs with an associated constant *)
+
+val start_lemma
+ : Id.t
+ -> ?pl:UState.universe_decl
+ -> goal_kind
+ -> Evd.evar_map
+ -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> proof_terminator)
+ -> ?sign:Environ.named_context_val
+ -> ?compute_guard:Proof_global.lemma_possible_guards
+ -> ?hook:declaration_hook
+ -> EConstr.types
+ -> t
+
+val start_dependent_lemma
+ : Id.t
+ -> ?pl:UState.universe_decl
+ -> goal_kind
+ -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> proof_terminator)
+ -> ?sign:Environ.named_context_val
+ -> ?compute_guard:Proof_global.lemma_possible_guards
+ -> ?hook:declaration_hook
+ -> Proofview.telescope
+ -> t
+
+val start_lemma_com
: program_mode:bool
-> ?inference_hook:Pretyping.inference_hook
-> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list
- -> Proof_global.t
-
-val start_proof_with_initialization :
- ?hook:declaration_hook ->
- goal_kind -> Evd.evar_map -> UState.universe_decl ->
- (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
- (Id.t (* name of thm *) *
- (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
- -> int list option -> Proof_global.t
+ -> t
-val standard_proof_terminator :
- ?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
- Proof_global.proof_terminator
+val start_lemma_with_initialization
+ : ?hook:declaration_hook
+ -> goal_kind -> Evd.evar_map -> UState.universe_decl
+ -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option
+ -> (Id.t (* name of thm *) *
+ (EConstr.types (* type of thm *) *
+ (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
+ -> int list option
+ -> t
-val fresh_name_for_anonymous_theorem : unit -> Id.t
+val default_thm_id : Names.Id.t
(* Prepare global named context for proof session: remove proofs of
opaque section definitions and remove vm-compiled code *)
val initialize_named_context_for_proof : unit -> Environ.named_context_val
-(** {6 ... } *)
+(** {6 Saving proofs } *)
-val save_proof_admitted
- : ?proof:Proof_global.closed_proof
- -> pstate:Proof_global.t
+val save_lemma_admitted
+ : ?proof:(Proof_global.proof_object * proof_terminator)
+ -> lemma:t
-> unit
-val save_proof_proved
- : ?proof:Proof_global.closed_proof
- -> ?ontop:Proof_global.stack
- -> opaque:Proof_global.opacity_flag
- -> idopt:Names.lident option
- -> Proof_global.stack option
-
-val save_pstate_proved
- : pstate:Proof_global.t
+val save_lemma_proved
+ : ?proof:(Proof_global.proof_object * proof_terminator)
+ -> ?lemma:t
-> opaque:Proof_global.opacity_flag
-> idopt:Names.lident option
-> unit
+
+(* API to build a terminator, should go away *)
+type proof_ending =
+ | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
+ | Proved of Proof_global.opacity_flag *
+ Names.lident option *
+ Proof_global.proof_object
+
+(** This stuff is internal and will be removed in the future. *)
+module Internal : sig
+
+ (** Only needed due to the Proof_global compatibility layer. *)
+ val get_terminator : t -> proof_terminator
+
+ (** Only needed by obligations, should be reified soon *)
+ val make_terminator : (proof_ending -> unit) -> proof_terminator
+ val apply_terminator : proof_terminator -> proof_ending -> unit
+
+end
diff --git a/vernac/locality.ml b/vernac/locality.ml
index 21be73b39c..465f04bc6e 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -12,10 +12,9 @@ open Decl_kinds
(** * Managing locality *)
-let local_of_bool = function
- | true -> Local
- | false -> Global
-
+let importability_of_bool = function
+ | true -> ImportNeedQualified
+ | false -> ImportDefaultBehavior
(** Positioning locality for commands supporting discharging and export
outside of modules *)
@@ -28,10 +27,22 @@ let make_non_locality = function Some false -> false | _ -> true
let make_locality = function Some true -> true | _ -> false
+let warn_local_declaration =
+ CWarnings.create ~name:"local-declaration" ~category:"scope"
+ Pp.(fun () ->
+ Pp.strbrk "Interpreting this declaration as if " ++
+ strbrk "a global declaration prefixed by \"Local\", " ++
+ strbrk "i.e. as a global declaration which shall not be " ++
+ strbrk "available without qualification when imported.")
+
let enforce_locality_exp locality_flag discharge =
match locality_flag, discharge with
- | Some b, NoDischarge -> local_of_bool b
- | None, NoDischarge -> Global
+ | Some b, NoDischarge -> Global (importability_of_bool b)
+ | None, NoDischarge -> Global ImportDefaultBehavior
+ | None, DoDischarge when not (Lib.sections_are_opened ()) ->
+ (* If a Let/Variable is defined outside a section, then we consider it as a local definition *)
+ warn_local_declaration ();
+ Global ImportNeedQualified
| None, DoDischarge -> Discharge
| Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case")
| Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case")
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 50914959dc..b96f500beb 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -732,13 +732,8 @@ type syntax_extension = {
synext_notgram : notation_grammar;
synext_unparsing : unparsing list;
synext_extra : (string * string) list;
- synext_compat : Flags.compat_version option;
}
-let is_active_compat = function
-| None -> true
-| Some v -> 0 <= Flags.version_compare v !Flags.compat_version
-
type syntax_extension_obj = locality_flag * syntax_extension
let check_and_extend_constr_grammar ntn rule =
@@ -759,7 +754,7 @@ let cache_one_syntax_extension se =
let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in
if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
with Not_found ->
- if is_active_compat se.synext_compat then begin
+ begin
(* Reserve the notation level *)
Notgram_ops.declare_notation_level ntn prec ~onlyprint;
(* Declare the parsing rule *)
@@ -934,10 +929,6 @@ let is_only_printing mods =
let test = function SetOnlyPrinting -> true | _ -> false in
List.exists test mods
-let get_compat_version mods =
- let test = function SetCompatVersion v -> Some v | _ -> None in
- try Some (List.find_map test mods) with Not_found -> None
-
(* Compute precedences from modifiers (or find default ones) *)
let set_entry_type from etyps (x,typ) =
@@ -1177,7 +1168,7 @@ module SynData = struct
(* Fields coming from the vernac-level modifiers *)
only_parsing : bool;
only_printing : bool;
- compat : Flags.compat_version option;
+ deprecation : Deprecation.t option;
format : lstring option;
extra : (string * string) list;
@@ -1222,12 +1213,32 @@ let check_locality_compatibility local custom i_typs =
strbrk " which is local."))
(List.uniquize allcustoms)
-let compute_syntax_data local df modifiers =
+let warn_deprecated_compat =
+ CWarnings.create ~name:"deprecated-compat" ~category:"deprecated"
+ (fun () -> Pp.(str"The \"compat\" modifier is deprecated." ++ spc () ++
+ str"Please use the \"deprecated\" attributed instead."))
+
+(* Returns the new deprecation and the onlyparsing status. This should be
+removed together with the compat syntax modifier. *)
+let merge_compat_deprecation compat deprecation =
+ match compat, deprecation with
+ | Some Flags.Current, _ -> deprecation, true
+ | Some _, Some _ ->
+ CErrors.user_err Pp.(str"The \"compat\" modifier cannot be used with the \"deprecated\" attribute."
+ ++ spc () ++ str"Please use only the latter.")
+ | Some v, None ->
+ warn_deprecated_compat ();
+ Some (Deprecation.make ~since:(Flags.pr_version v) ()), true
+ | None, Some _ -> deprecation, true
+ | None, None -> deprecation, false
+
+let compute_syntax_data ~local deprecation df modifiers =
let open SynData in
let open NotationMods in
let mods = interp_modifiers modifiers in
let onlyprint = mods.only_printing in
let onlyparse = mods.only_parsing in
+ let deprecation, _ = merge_compat_deprecation mods.compat deprecation in
if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in
let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
@@ -1265,7 +1276,7 @@ let compute_syntax_data local df modifiers =
only_parsing = mods.only_parsing;
only_printing = mods.only_printing;
- compat = mods.compat;
+ deprecation;
format = mods.format;
extra = mods.extra;
@@ -1281,9 +1292,9 @@ let compute_syntax_data local df modifiers =
not_data = sy_fulldata;
}
-let compute_pure_syntax_data local df mods =
+let compute_pure_syntax_data ~local df mods =
let open SynData in
- let sd = compute_syntax_data local df mods in
+ let sd = compute_syntax_data ~local None df mods in
let msgs =
if sd.only_parsing then
(Feedback.msg_warning ?loc:None,
@@ -1301,7 +1312,7 @@ type notation_obj = {
notobj_coercion : entry_coercion_kind option;
notobj_onlyparse : bool;
notobj_onlyprint : bool;
- notobj_compat : Flags.compat_version option;
+ notobj_deprecation : Deprecation.t option;
notobj_notation : notation * notation_location;
}
@@ -1323,11 +1334,11 @@ let open_notation i (_, nobj) =
let (ntn, df) = nobj.notobj_notation in
let pat = nobj.notobj_interp in
let onlyprint = nobj.notobj_onlyprint in
+ let deprecation = nobj.notobj_deprecation in
let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
- let active = is_active_compat nobj.notobj_compat in
- if Int.equal i 1 && fresh && active then begin
+ if Int.equal i 1 && fresh then begin
(* Declare the interpretation *)
- let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in
+ let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
(* Declare the uninterpretation *)
if not nobj.notobj_onlyparse then
Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat;
@@ -1388,7 +1399,6 @@ let recover_notation_syntax ntn =
synext_notgram = pa_rule;
synext_unparsing = pp_rule;
synext_extra = pp_extra_rules;
- synext_compat = None;
}
with Not_found ->
raise NoSyntaxRule
@@ -1437,7 +1447,6 @@ let make_syntax_rules (sd : SynData.syn_data) = let open SynData in
synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
synext_unparsing = pp_rule;
synext_extra = sd.extra;
- synext_compat = sd.compat;
}
(**********************************************************************)
@@ -1447,9 +1456,9 @@ let to_map l =
let fold accu (x, v) = Id.Map.add x v accu in
List.fold_left fold Id.Map.empty l
-let add_notation_in_scope local df env c mods scope =
+let add_notation_in_scope ~local deprecation df env c mods scope =
let open SynData in
- let sd = compute_syntax_data local df mods in
+ let sd = compute_syntax_data ~local deprecation df mods in
(* Prepare the interpretation *)
(* Prepare the parsing and printing rules *)
let sy_rules = make_syntax_rules sd in
@@ -1470,7 +1479,7 @@ let add_notation_in_scope local df env c mods scope =
notobj_onlyparse = onlyparse;
notobj_coercion = coe;
notobj_onlyprint = sd.only_printing;
- notobj_compat = sd.compat;
+ notobj_deprecation = sd.deprecation;
notobj_notation = sd.info;
} in
(* Ready to change the global state *)
@@ -1479,7 +1488,7 @@ let add_notation_in_scope local df env c mods scope =
Lib.add_anonymous_leaf (inNotation notation);
sd.info
-let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
+let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint deprecation =
let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in
(* Recover types of variables and pa/pp rules; redeclare them if needed *)
let level, i_typs, onlyprint = if not (is_numeral symbs) then begin
@@ -1510,7 +1519,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
notobj_onlyparse = onlyparse;
notobj_coercion = coe;
notobj_onlyprint = onlyprint;
- notobj_compat = compat;
+ notobj_deprecation = deprecation;
notobj_notation = df';
} in
Lib.add_anonymous_leaf (inNotation notation);
@@ -1518,41 +1527,40 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
(* Notations without interpretation (Reserved Notation) *)
-let add_syntax_extension local ({CAst.loc;v=df},mods) = let open SynData in
- let psd = compute_pure_syntax_data local df mods in
- let sy_rules = make_syntax_rules {psd with compat = None} in
+let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in
+ let psd = compute_pure_syntax_data ~local df mods in
+ let sy_rules = make_syntax_rules {psd with deprecation = None} in
Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs;
Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
(* Notations with only interpretation *)
let add_notation_interpretation env ({CAst.loc;v=df},c,sc) =
- let df' = add_notation_interpretation_core false df env c sc false false None in
+ let df' = add_notation_interpretation_core ~local:false df env c sc false false None in
Dumpglob.dump_notation (loc,df') sc true
let set_notation_for_interpretation env impls ({CAst.v=df},c,sc) =
(try ignore
- (Flags.silently (fun () -> add_notation_interpretation_core false df env ~impls c sc false false None) ());
+ (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc false false None) ());
with NoSyntaxRule ->
user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
(* Main entry point *)
-let add_notation local env c ({CAst.loc;v=df},modifiers) sc =
+let add_notation ~local deprecation env c ({CAst.loc;v=df},modifiers) sc =
let df' =
if no_syntax_modifiers modifiers then
(* No syntax data: try to rely on a previously declared rule *)
let onlyparse = is_only_parsing modifiers in
let onlyprint = is_only_printing modifiers in
- let compat = get_compat_version modifiers in
- try add_notation_interpretation_core local df env c sc onlyparse onlyprint compat
+ try add_notation_interpretation_core ~local df env c sc onlyparse onlyprint deprecation
with NoSyntaxRule ->
(* Try to determine a default syntax rule *)
- add_notation_in_scope local df env c modifiers sc
+ add_notation_in_scope ~local deprecation df env c modifiers sc
else
(* Declare both syntax and interpretation *)
- add_notation_in_scope local df env c modifiers sc
+ add_notation_in_scope ~local deprecation df env c modifiers sc
in
Dumpglob.dump_notation (loc,df') sc true
@@ -1566,7 +1574,7 @@ let add_notation_extra_printing_rule df k v =
let inject_var x = CAst.make @@ CRef (qualid_of_ident x,None)
-let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
+let add_infix ~local deprecation env ({CAst.loc;v=inf},modifiers) pr sc =
check_infix_modifiers modifiers;
(* check the precedence *)
let vars = names_of_constr_expr pr in
@@ -1575,7 +1583,7 @@ let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
let metas = [inject_var x; inject_var y] in
let c = mkAppC (pr,metas) in
let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in
- add_notation local env c (df,modifiers) sc
+ add_notation ~local deprecation env c (df,modifiers) sc
(**********************************************************************)
(* Scopes, delimiters and classes bound to scopes *)
@@ -1651,7 +1659,7 @@ let try_interp_name_alias = function
| [], { CAst.v = CRef (ref,_) } -> intern_reference ref
| _ -> raise Not_found
-let add_syntactic_definition env ident (vars,c) local onlyparse =
+let add_syntactic_definition ~local deprecation env ident (vars,c) compat =
let vars,reversibility,pat =
try [], APrioriReversible, NRef (try_interp_name_alias (vars,c))
with Not_found ->
@@ -1665,11 +1673,9 @@ let add_syntactic_definition env ident (vars,c) local onlyparse =
let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in
List.map map vars, reversibility, pat
in
- let onlyparse = match onlyparse with
- | None when fst (printability None false reversibility pat) -> Some Flags.Current
- | p -> p
- in
- Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
+ let deprecation, onlyparsing = merge_compat_deprecation compat deprecation in
+ let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in
+ Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat)
(**********************************************************************)
(* Declaration of custom entry *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 6435df23c7..6532cee367 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -19,10 +19,10 @@ val add_token_obj : string -> unit
(** Adding a (constr) notation in the environment*)
-val add_infix : locality_flag -> env -> (lstring * syntax_modifier list) ->
+val add_infix : local:bool -> Deprecation.t option -> env -> (lstring * syntax_modifier list) ->
constr_expr -> scope_name option -> unit
-val add_notation : locality_flag -> env -> constr_expr ->
+val add_notation : local:bool -> Deprecation.t option -> env -> constr_expr ->
(lstring * syntax_modifier list) -> scope_name option -> unit
val add_notation_extra_printing_rule : string -> string -> string -> unit
@@ -47,12 +47,12 @@ val set_notation_for_interpretation : env -> Constrintern.internalization_env ->
(** Add only the parsing/printing rule of a notation *)
val add_syntax_extension :
- locality_flag -> (lstring * syntax_modifier list) -> unit
+ local:bool -> (lstring * syntax_modifier list) -> unit
(** Add a syntactic definition (as in "Notation f := ...") *)
-val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr ->
- bool -> Flags.compat_version option -> unit
+val add_syntactic_definition : local:bool -> Deprecation.t option -> env ->
+ Id.t -> Id.t list * constr_expr -> Flags.compat_version option -> unit
(** Print the Camlp5 state of a grammar *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 0d93e19723..50d24c20c9 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -497,7 +497,7 @@ let compute_possible_guardness_evidences n fixbody fixtype =
let ctx = fst (decompose_prod_n_assum m fixtype) in
List.map_i (fun i _ -> i) 0 ctx
-let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants)
+let mk_proof c = ((c, Univ.ContextSet.empty), Evd.empty_side_effects)
let declare_mutual_definition l =
let len = List.length l in
@@ -632,7 +632,7 @@ let declare_obligation prg obl body ty uctx =
if get_shrink_obligations () && not poly then
shrink_body body ty else [], body, ty, [||]
in
- let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+ let body = ((body,Univ.ContextSet.empty), Evd.empty_side_effects) in
let ce =
{ const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
const_entry_secctx = None;
@@ -643,7 +643,7 @@ let declare_obligation prg obl body ty uctx =
const_entry_feedback = None;
} in
(* ppedrot: seems legit to have obligations as local *)
- let constant = Declare.declare_constant obl.obl_name ~local:true
+ let constant = Declare.declare_constant obl.obl_name ~local:ImportNeedQualified
(DefinitionEntry ce,IsProof Property)
in
if not opaque then add_hint (Locality.make_section_locality None) prg constant;
@@ -787,9 +787,11 @@ let dependencies obls n =
obls;
!res
-let goal_kind poly = Decl_kinds.Local, poly, Decl_kinds.DefinitionBody Decl_kinds.Definition
+let goal_kind poly =
+ Decl_kinds.(Global ImportNeedQualified, poly, DefinitionBody Definition)
-let goal_proof_kind poly = Decl_kinds.Local, poly, Decl_kinds.Proof Decl_kinds.Lemma
+let goal_proof_kind poly =
+ Decl_kinds.(Global ImportNeedQualified, poly, Proof Lemma)
let kind_of_obligation poly o =
match o with
@@ -820,8 +822,8 @@ let solve_by_tac ?loc name evi t poly ctx =
Pfedit.build_constant_by_tactic
id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in
let env = Global.env () in
- let body = Future.force entry.const_entry_body in
- let body = Safe_typing.inline_private_constants env body in
+ let (body, eff) = Future.force entry.const_entry_body in
+ let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body));
Some (fst body, entry.const_entry_type, Evd.evar_universe_context ctx')
@@ -839,14 +841,15 @@ let solve_by_tac ?loc name evi t poly ctx =
let obligation_terminator ?hook name num guard auto pf =
let open Proof_global in
- let term = Lemmas.standard_proof_terminator ?hook guard in
+ let open Lemmas in
+ let term = standard_proof_terminator ?hook guard in
match pf with
- | Admitted _ -> apply_terminator term pf
+ | Admitted _ -> Internal.apply_terminator term pf
| Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
let env = Global.env () in
let ty = entry.Entries.const_entry_type in
- let body = Future.force entry.const_entry_body in
- let (body, cstr) = Safe_typing.inline_private_constants env body in
+ let body, eff = Future.force entry.const_entry_body in
+ let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
let sigma = Evd.from_ctx uctx in
let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body);
@@ -962,13 +965,13 @@ let rec solve_obligation prg num tac =
let evd = Evd.update_sigma_env evd (Global.env ()) in
let auto n tac oblset = auto_solve_obligations n ~oblset tac in
let terminator ?hook guard =
- Proof_global.make_terminator
+ Lemmas.Internal.make_terminator
(obligation_terminator prg.prg_name num guard ?hook auto) in
let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
- let pstate = Lemmas.start_proof ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
- let pstate = fst @@ Pfedit.by !default_tactic pstate in
- let pstate = Option.cata (fun tac -> Proof_global.set_endline_tactic tac pstate) pstate tac in
- pstate
+ let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
+ let lemma = fst @@ Lemmas.by !default_tactic lemma in
+ let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in
+ lemma
and obligation (user_num, name, typ) tac =
let num = pred user_num in
@@ -1102,7 +1105,7 @@ let show_term n =
++ Printer.pr_constr_env env sigma prg.prg_body)
let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
- ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+ ?(implicits=[]) ?(kind=Global ImportDefaultBehavior,false,Definition) ?tactic
?(reduce=reduce) ?hook ?(opaque = false) obls =
let sign = Lemmas.initialize_named_context_for_proof () in
let info = Id.print n ++ str " has type-checked" in
@@ -1122,7 +1125,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
| _ -> res)
let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
- ?(kind=Global,false,Definition) ?(reduce=reduce)
+ ?(kind=Global ImportDefaultBehavior,false,Definition) ?(reduce=reduce)
?hook ?(opaque = false) notations fixkind =
let sign = Lemmas.initialize_named_context_for_proof () in
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
@@ -1153,7 +1156,7 @@ let admit_prog prg =
| None ->
let x = subst_deps_obl obls x in
let ctx = UState.univ_entry ~poly:false prg.prg_ctx in
- let kn = Declare.declare_constant x.obl_name ~local:true
+ let kn = Declare.declare_constant x.obl_name ~local:ImportNeedQualified
(ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural)
in
assumption_message x.obl_name;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 3b77039de5..8734d82970 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -86,14 +86,14 @@ val add_mutual_definitions :
fixpoint_kind -> unit
val obligation
- : int * Names.Id.t option * Constrexpr.constr_expr option
+ : int * Names.Id.t option * Constrexpr.constr_expr option
-> Genarg.glob_generic_argument option
- -> Proof_global.t
+ -> Lemmas.t
val next_obligation
- : Names.Id.t option
+ : Names.Id.t option
-> Genarg.glob_generic_argument option
- -> Proof_global.t
+ -> Lemmas.t
val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress
(* Number of remaining obligations to be solved for this program *)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 02af1904fd..fda1e2afea 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -359,6 +359,8 @@ open Pputils
keyword (if many then "Variables" else "Variable")
| (DoDischarge,Conjectural) ->
anomaly (Pp.str "Don't know how to beautify a local conjecture.")
+ | (_,Context) ->
+ anomaly (Pp.str "Context is used only internally.")
let pr_params pr_c (xl,(c,t)) =
hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
diff --git a/vernac/record.ml b/vernac/record.ml
index 6101e13edd..c777ef2c2b 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -344,7 +344,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f
try
let entry = {
const_entry_body =
- Future.from_val (Safe_typing.mk_pure_proof proj);
+ Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects);
const_entry_secctx = None;
const_entry_type = Some projtyp;
const_entry_universes = ctx;
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 8668f01053..112c4b6451 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -38,28 +38,24 @@ module NamedDecl = Context.Named.Declaration
let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
let debug = false
+
(* XXX Should move to a common library *)
let vernac_pperr_endline pp =
if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else ()
-(* Misc *)
-
-let there_are_pending_proofs ~pstate =
- not Option.(is_empty pstate)
+(* Utility functions, at some point they should all disappear and
+ instead enviroment/state selection should be done at the Vernac DSL
+ level. *)
-(* EJGA: Only used in close_proof 2, can remove once ?proof hack is away *)
-let vernac_require_open_proof ~pstate f =
- match pstate with
- | Some pstate -> f ~pstate
+(* EJGA: Only used in close_proof, can remove once the ?proof hack is no more *)
+let vernac_require_open_lemma ~stack f =
+ match stack with
+ | Some stack -> f ~stack
| None -> user_err Pp.(str "Command not supported (No proof-editing in progress)")
-let with_pstate ~pstate f =
- vernac_require_open_proof ~pstate
- (fun ~pstate -> f ~pstate:(Proof_global.get_current_pstate pstate))
-
- let modify_pstate ~pstate f =
- vernac_require_open_proof ~pstate (fun ~pstate ->
- Some (Proof_global.modify_current_pstate (fun pstate -> f ~pstate) pstate))
+let with_pstate ~stack f =
+ vernac_require_open_lemma ~stack
+ (fun ~stack -> Stack.with_top_pstate stack ~f:(fun pstate -> f ~pstate))
let get_current_or_global_context ~pstate =
match pstate with
@@ -85,7 +81,7 @@ module DefAttributes = struct
locality : bool option;
polymorphic : bool;
program : bool;
- deprecated : deprecation option;
+ deprecated : Deprecation.t option;
}
let parse f =
@@ -96,6 +92,8 @@ module DefAttributes = struct
{ polymorphic; program; locality; deprecated }
end
+let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
+
let with_locality ~atts f =
let local = Attributes.(parse locality atts) in
f ~local
@@ -106,8 +104,7 @@ let with_section_locality ~atts f =
f ~section_local
let with_module_locality ~atts f =
- let local = Attributes.(parse locality atts) in
- let module_local = make_module_locality local in
+ let module_local = Attributes.(parse module_locality atts) in
f ~module_local
let with_def_attributes ~atts f =
@@ -122,7 +119,7 @@ let show_proof ~pstate =
(* spiwack: this would probably be cooler with a bit of polishing. *)
try
let pstate = Option.get pstate in
- let p = Proof_global.give_me_the_proof pstate in
+ let p = Proof_global.get_proof pstate in
let sigma, env = Pfedit.get_current_context pstate in
let pprf = Proof.partial_proof p in
Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
@@ -132,24 +129,21 @@ let show_proof ~pstate =
| Option.IsNone ->
user_err (str "No goals to show.")
-let show_top_evars ~pstate =
+let show_top_evars ~proof =
(* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
- let pfts = Proof_global.give_me_the_proof pstate in
- let Proof.{goals;shelf;given_up;sigma} = Proof.data pfts in
+ let Proof.{goals;shelf;given_up;sigma} = Proof.data proof in
pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma)
-let show_universes ~pstate =
- let pfts = Proof_global.give_me_the_proof pstate in
- let Proof.{goals;sigma} = Proof.data pfts in
+let show_universes ~proof =
+ let Proof.{goals;sigma} = Proof.data proof in
let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in
Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++
str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx
(* Simulate the Intro(s) tactic *)
-let show_intro ~pstate all =
+let show_intro ~proof all =
let open EConstr in
- let pf = Proof_global.give_me_the_proof pstate in
- let Proof.{goals;sigma} = Proof.data pf in
+ let Proof.{goals;sigma} = Proof.data proof in
if not (List.is_empty goals) then begin
let gl = {Evd.it=List.hd goals ; sigma = sigma; } in
let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in
@@ -511,7 +505,7 @@ let dump_global r =
let vernac_syntax_extension ~module_local infix l =
if infix then Metasyntax.check_infix_modifiers (snd l);
- Metasyntax.add_syntax_extension module_local l
+ Metasyntax.add_syntax_extension ~local:module_local l
let vernac_declare_scope ~module_local sc =
Metasyntax.declare_scope module_local sc
@@ -530,11 +524,13 @@ let vernac_open_close_scope ~section_local (b,s) =
let vernac_arguments_scope ~section_local r scl =
Notation.declare_arguments_scope section_local (smart_global r) scl
-let vernac_infix ~module_local =
- Metasyntax.add_infix module_local (Global.env())
+let vernac_infix ~atts =
+ let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
+ Metasyntax.add_infix ~local:module_local deprecation (Global.env())
-let vernac_notation ~module_local =
- Metasyntax.add_notation module_local (Global.env())
+let vernac_notation ~atts =
+ let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
+ Metasyntax.add_notation ~local:module_local deprecation (Global.env())
let vernac_custom_entry ~module_local s =
Metasyntax.declare_custom_entry module_local s
@@ -586,7 +582,7 @@ let start_proof_and_print ~program_mode ?hook k l =
in Some hook
else None
in
- start_proof_com ~program_mode ?inference_hook ?hook k l
+ start_lemma_com ~program_mode ?inference_hook ?hook k l
let vernac_definition_hook p = function
| Coercion ->
@@ -597,6 +593,9 @@ let vernac_definition_hook p = function
Some (Class.add_subclass_hook p)
| _ -> None
+let fresh_name_for_anonymous_theorem () =
+ Namegen.next_global_ident_away Lemmas.default_thm_id Id.Set.empty
+
let vernac_definition_name lid local =
let lid =
match lid with
@@ -606,7 +605,7 @@ let vernac_definition_name lid local =
let () =
match local with
| Discharge -> Dumpglob.dump_definition lid true "var"
- | Local | Global -> Dumpglob.dump_definition lid false "def"
+ | Global _ -> Dumpglob.dump_definition lid false "def"
in
lid
@@ -641,30 +640,39 @@ let vernac_start_proof ~atts kind l =
List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l
-let vernac_end_proof ?pstate:ontop ?proof = function
+let vernac_end_proof ?stack ?proof = let open Vernacexpr in function
| Admitted ->
- with_pstate ~pstate:ontop (save_proof_admitted ?proof);
- ontop
+ vernac_require_open_lemma ~stack (fun ~stack ->
+ let lemma, stack = Stack.pop stack in
+ save_lemma_admitted ?proof ~lemma;
+ stack)
| Proved (opaque,idopt) ->
- save_proof_proved ?ontop ?proof ~opaque ~idopt
+ let lemma, stack = match stack with
+ | None -> None, None
+ | Some stack ->
+ let lemma, stack = Stack.pop stack in
+ Some lemma, stack
+ in
+ save_lemma_proved ?lemma ?proof ~opaque ~idopt;
+ stack
-let vernac_exact_proof ~pstate c =
+let vernac_exact_proof ~lemma c =
(* spiwack: for simplicity I do not enforce that "Proof proof_term" is
called only at the beginning of a proof. *)
- let pstate, status = Pfedit.by (Tactics.exact_proof c) pstate in
- let () = save_pstate_proved ~pstate ~opaque:Proof_global.Opaque ~idopt:None in
+ let lemma, status = Lemmas.by (Tactics.exact_proof c) lemma in
+ let () = save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Opaque ~idopt:None in
if not status then Feedback.feedback Feedback.AddedAxiom
let vernac_assumption ~atts discharge kind l nl =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
- let global = local == Global in
let kind = local, atts.polymorphic, kind in
List.iter (fun (is_coe,(idl,c)) ->
if Dumpglob.dump () then
List.iter (fun (lid, _) ->
- if global then Dumpglob.dump_definition lid false "ax"
- else Dumpglob.dump_definition lid true "var") idl) l;
+ match local with
+ | Global _ -> Dumpglob.dump_definition lid false "ax"
+ | Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in
if not status then Feedback.feedback Feedback.AddedAxiom
@@ -1157,7 +1165,7 @@ let focus_command_cond = Proof.no_cond command_focus
all tactics fail if there are no further goals to prove. *)
let vernac_solve_existential ~pstate n com =
- Proof_global.modify_proof (fun p ->
+ Proof_global.map_proof (fun p ->
let intern env sigma = Constrintern.intern_constr env sigma com in
Proof.V82.instantiate_evar (Global.env ()) n intern p) pstate
@@ -1167,15 +1175,14 @@ let vernac_set_end_tac ~pstate tac =
(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
Proof_global.set_endline_tactic tac pstate
-let vernac_set_used_variables ~(pstate : Proof_global.t) e : Proof_global.t =
+let vernac_set_used_variables ~pstate e : Proof_global.t =
let env = Global.env () in
let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
- let tys =
- List.map snd (initial_goals (Proof_global.give_me_the_proof pstate)) in
+ let tys = List.map snd (initial_goals (Proof_global.get_proof pstate)) in
let tys = List.map EConstr.Unsafe.to_constr tys in
let l = Proof_using.process_expr env e tys in
let vars = Environ.named_context env in
- List.iter (fun id ->
+ List.iter (fun id ->
if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
user_err ~hdr:"vernac_set_used_variables"
(str "Unknown variable: " ++ Id.print id))
@@ -1261,9 +1268,10 @@ let vernac_hints ~atts dbnames h =
let local = enforce_module_locality local in
Hints.add_hints ~local dbnames (Hints.interp_hints poly h)
-let vernac_syntactic_definition ~module_local lid x y =
+let vernac_syntactic_definition ~atts lid x compat =
+ let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
Dumpglob.dump_definition lid false "syndef";
- Metasyntax.add_syntactic_definition (Global.env()) lid.v x module_local y
+ Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x compat
let cache_bidi_hints (_name, (gr, ohint)) =
match ohint with
@@ -1878,10 +1886,10 @@ let get_current_context_of_args ~pstate =
match pstate with
| None -> fun _ ->
let env = Global.env () in Evd.(from_env env, env)
- | Some pstate ->
+ | Some lemma ->
function
- | Some n -> Pfedit.get_goal_context pstate n
- | None -> Pfedit.get_current_context pstate
+ | Some n -> Pfedit.get_goal_context lemma n
+ | None -> Pfedit.get_current_context lemma
let query_command_selector ?loc = function
| None -> None
@@ -1946,7 +1954,7 @@ let vernac_global_check c =
let get_nth_goal ~pstate n =
- let pf = Proof_global.give_me_the_proof pstate in
+ let pf = Proof_global.get_proof pstate in
let Proof.{goals;sigma} = Proof.data pf in
let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in
gl
@@ -2022,9 +2030,9 @@ let vernac_print ~pstate ~atts =
| PrintHintGoal ->
begin match pstate with
| Some pstate ->
- Hints.pr_applicable_hint pstate
+ Hints.pr_applicable_hint pstate
| None ->
- str "No proof in progress"
+ str "No proof in progress"
end
| PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s
| PrintHintDb -> Hints.pr_searchtable env sigma
@@ -2176,7 +2184,7 @@ let vernac_register qid r =
(* Proof management *)
let vernac_focus ~pstate gln =
- Proof_global.modify_proof (fun p ->
+ Proof_global.map_proof (fun p ->
match gln with
| None -> Proof.focus focus_command_cond () 1 p
| Some 0 ->
@@ -2187,19 +2195,18 @@ let vernac_focus ~pstate gln =
(* Unfocuses one step in the focus stack. *)
let vernac_unfocus ~pstate =
- Proof_global.modify_proof
+ Proof_global.map_proof
(fun p -> Proof.unfocus command_focus p ())
pstate
(* Checks that a proof is fully unfocused. Raises an error if not. *)
let vernac_unfocused ~pstate =
- let p = Proof_global.give_me_the_proof pstate in
+ let p = Proof_global.get_proof pstate in
if Proof.unfocused p then
str"The proof is indeed fully unfocused."
else
user_err Pp.(str "The proof is not fully unfocused.")
-
(* "{" focuses on the first goal, "n: {" focuses on the n-th goal
"}" unfocuses, provided that the proof of the goal has been completed.
*)
@@ -2207,7 +2214,7 @@ let subproof_kind = Proof.new_focus_kind ()
let subproof_cond = Proof.done_cond subproof_kind
let vernac_subproof gln ~pstate =
- Proof_global.modify_proof (fun p ->
+ Proof_global.map_proof (fun p ->
match gln with
| None -> Proof.focus subproof_cond () 1 p
| Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
@@ -2217,12 +2224,12 @@ let vernac_subproof gln ~pstate =
pstate
let vernac_end_subproof ~pstate =
- Proof_global.modify_proof (fun p ->
+ Proof_global.map_proof (fun p ->
Proof.unfocus subproof_kind p ())
pstate
let vernac_bullet (bullet : Proof_bullet.t) ~pstate =
- Proof_global.modify_proof (fun p ->
+ Proof_global.map_proof (fun p ->
Proof_bullet.put p bullet) pstate
(* Stack is needed due to show proof names, should deprecate / remove
@@ -2239,25 +2246,26 @@ let vernac_show ~pstate =
end
(* Show functions that require a proof state *)
| Some pstate ->
+ let proof = Proof_global.get_proof pstate in
begin function
| ShowGoal goalref ->
- let proof = Proof_global.give_me_the_proof pstate in
begin match goalref with
| OpenSubgoals -> pr_open_subgoals ~proof
| NthGoal n -> pr_nth_open_subgoal ~proof n
| GoalId id -> pr_goal_by_id ~proof id
end
- | ShowExistentials -> show_top_evars ~pstate
- | ShowUniverses -> show_universes ~pstate
+ | ShowExistentials -> show_top_evars ~proof
+ | ShowUniverses -> show_universes ~proof
+ (* Deprecate *)
| ShowProofNames ->
- Id.print (Proof_global.get_current_proof_name pstate)
- | ShowIntros all -> show_intro ~pstate all
+ Id.print (Proof_global.get_proof_name pstate)
+ | ShowIntros all -> show_intro ~proof all
| ShowProof -> show_proof ~pstate:(Some pstate)
| ShowMatch id -> show_match id
end
let vernac_check_guard ~pstate =
- let pts = Proof_global.give_me_the_proof pstate in
+ let pts = Proof_global.get_proof pstate in
let pfterm = List.hd (Proof.partial_proof pts) in
let message =
try
@@ -2322,30 +2330,31 @@ let locate_if_not_already ?loc (e, info) =
exception End_of_input
-let interp_typed_vernac c ~pstate =
- let open Proof_global in
+let interp_typed_vernac c ~stack =
let open Vernacextend in
match c with
- | VtDefault f -> f (); pstate
+ | VtDefault f -> f (); stack
| VtNoProof f ->
- if there_are_pending_proofs ~pstate then
+ if Option.has_some stack then
user_err Pp.(str "Command not supported (Open proofs remain)");
let () = f () in
- pstate
+ stack
| VtCloseProof f ->
- vernac_require_open_proof ~pstate (fun ~pstate ->
- f ~pstate:(Proof_global.get_current_pstate pstate);
- Proof_global.discard_current pstate)
+ vernac_require_open_lemma ~stack (fun ~stack ->
+ let lemma, stack = Stack.pop stack in
+ f ~lemma;
+ stack)
| VtOpenProof f ->
- Some (push ~ontop:pstate (f ()))
+ Some (Stack.push stack (f ()))
| VtModifyProof f ->
- modify_pstate f ~pstate
+ Option.map (Stack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack
| VtReadProofOpt f ->
- f ~pstate:(Option.map get_current_pstate pstate);
- pstate
+ let pstate = Option.map (Stack.with_top_pstate ~f:(fun x -> x)) stack in
+ f ~pstate;
+ stack
| VtReadProof f ->
- with_pstate ~pstate f;
- pstate
+ with_pstate ~stack f;
+ stack
(* We interpret vernacular commands to a DSL that specifies their
allowed actions on proof states *)
@@ -2374,9 +2383,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
| VernacOpenCloseScope (b, s) ->
VtDefault(fun () -> with_section_locality ~atts vernac_open_close_scope (b,s))
| VernacInfix (mv,qid,sc) ->
- VtDefault(fun () -> with_module_locality ~atts vernac_infix mv qid sc)
+ VtDefault(fun () -> vernac_infix ~atts mv qid sc)
| VernacNotation (c,infpl,sc) ->
- VtDefault(fun () -> with_module_locality ~atts vernac_notation c infpl sc)
+ VtDefault(fun () -> vernac_notation ~atts c infpl sc)
| VernacNotationAddFormat(n,k,v) ->
VtDefault(fun () ->
unsupported_attributes atts;
@@ -2398,9 +2407,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
| VernacStartTheoremProof (k,l) ->
VtOpenProof(fun () -> with_def_attributes ~atts vernac_start_proof k l)
| VernacExactProof c ->
- VtCloseProof(fun ~pstate ->
+ VtCloseProof (fun ~lemma ->
unsupported_attributes atts;
- vernac_exact_proof ~pstate c)
+ vernac_exact_proof ~lemma c)
| VernacDefineModule (export,lid,bl,mtys,mexprl) ->
let i () =
@@ -2554,8 +2563,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
VtDefault(fun () ->
vernac_hints ~atts dbnames hints)
| VernacSyntacticDefinition (id,c,b) ->
- VtDefault(fun () ->
- with_module_locality ~atts vernac_syntactic_definition id c b)
+ VtDefault(fun () -> vernac_syntactic_definition ~atts id c b)
| VernacArguments (qid, args, more_implicits, nargs, bidi, flags) ->
VtDefault(fun () ->
with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags))
@@ -2671,7 +2679,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
* still parsed as the obsolete_locality grammar entry for retrocompatibility.
* loc is the Loc.t of the vernacular command being interpreted. *)
let rec interp_expr ?proof ~atts ~st c =
- let pstate = st.Vernacstate.proof in
+ let stack = st.Vernacstate.lemmas in
vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
match c with
@@ -2699,11 +2707,11 @@ let rec interp_expr ?proof ~atts ~st c =
(* Special: ?proof parameter doesn't allow for uniform pstate pop :S *)
| VernacEndProof e ->
unsupported_attributes atts;
- vernac_end_proof ?proof ?pstate e
+ vernac_end_proof ?proof ?stack e
| v ->
let fv = translate_vernac ~atts v in
- interp_typed_vernac ~pstate fv
+ interp_typed_vernac ~stack fv
(* XXX: This won't properly set the proof mode, as of today, it is
controlled by the STM. Thus, we would need access information from
@@ -2712,8 +2720,9 @@ let rec interp_expr ?proof ~atts ~st c =
without a considerable amount of refactoring.
*)
and vernac_load ~verbosely ~st fname =
- let pstate = st.Vernacstate.proof in
- if there_are_pending_proofs ~pstate then
+ let there_are_pending_proofs ~stack = not Option.(is_empty stack) in
+ let stack = st.Vernacstate.lemmas in
+ if there_are_pending_proofs ~stack then
CErrors.user_err Pp.(str "Load is not supported inside proofs.");
(* Open the file *)
let fname =
@@ -2730,29 +2739,29 @@ and vernac_load ~verbosely ~st fname =
match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with
| Some x -> x
| None -> raise End_of_input) in
- let rec load_loop ~pstate =
+ let rec load_loop ~stack =
try
- let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) pstate in
- let pstate =
- v_mod (interp_control ?proof:None ~st:{ st with Vernacstate.proof = pstate })
+ let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in
+ let stack =
+ v_mod (interp_control ?proof:None ~st:{ st with Vernacstate.lemmas = stack })
(parse_sentence proof_mode input) in
- load_loop ~pstate
+ load_loop ~stack
with
End_of_input ->
- pstate
+ stack
in
- let pstate = load_loop ~pstate in
+ let stack = load_loop ~stack in
(* If Load left a proof open, we fail too. *)
- if there_are_pending_proofs ~pstate then
+ if there_are_pending_proofs ~stack then
CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
- pstate
+ stack
and interp_control ?proof ~st v = match v with
| { v=VernacExpr (atts, cmd) } ->
interp_expr ?proof ~atts ~st cmd
| { v=VernacFail v } ->
with_fail ~st (fun () -> interp_control ?proof ~st v);
- st.Vernacstate.proof
+ st.Vernacstate.lemmas
| { v=VernacTimeout (timeout,v) } ->
vernac_timeout ~timeout (interp_control ?proof ~st) v
| { v=VernacRedirect (s, v) } ->
@@ -2774,8 +2783,8 @@ let interp ?(verbosely=true) ?proof ~st cmd =
Vernacstate.unfreeze_interp_state st;
try vernac_timeout (fun st ->
let v_mod = if verbosely then Flags.verbosely else Flags.silently in
- let pstate = v_mod (interp_control ?proof ~st) cmd in
- Vernacstate.Proof_global.set pstate [@ocaml.warning "-3"];
+ let ontop = v_mod (interp_control ?proof ~st) cmd in
+ Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"];
Vernacstate.freeze_interp_state ~marshallable:false
) st
with exn ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index d94ddc1aaf..f1c8b29313 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -22,7 +22,7 @@ val vernac_require :
(** The main interpretation function of vernacular expressions *)
val interp :
?verbosely:bool ->
- ?proof:Proof_global.closed_proof ->
+ ?proof:(Proof_global.proof_object * Lemmas.proof_terminator) ->
st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
(** Prepare a "match" template for a given inductive type.
@@ -41,13 +41,6 @@ val command_focus : unit Proof.focus_kind
val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
Evd.evar_map * Redexpr.red_expr) Hook.t
-(** Helper *)
-val vernac_require_open_proof : pstate:Proof_global.stack option -> (pstate:Proof_global.stack -> 'a) -> 'a
-
-val with_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.t -> 'a) -> 'a
-
-val modify_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.t -> Proof_global.t) -> Proof_global.stack option
-
(* Flag set when the test-suite is called. Its only effect to display
verbose information for `Fail` *)
val test_mode : bool ref
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 6f8a4e8a3c..c7008c2a84 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -16,7 +16,11 @@ type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque
type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop
-type vernac_type =
+type vernac_when =
+ | VtNow
+ | VtLater
+
+type vernac_classification =
(* Start of a proof *)
| VtStartProof of vernac_start
(* Command altering the global state, bad for parallel
@@ -37,7 +41,7 @@ type vernac_type =
(* To be removed *)
| VtMeta
and vernac_start = opacity_guarantee * Names.Id.t list
-and vernac_sideff_type = Names.Id.t list
+and vernac_sideff_type = Names.Id.t list * vernac_when
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
| Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
@@ -48,16 +52,12 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *)
and proof_block_name = string (** open type of delimiters *)
-type vernac_when =
- | VtNow
- | VtLater
-type vernac_classification = vernac_type * vernac_when
-
type typed_vernac =
| VtDefault of (unit -> unit)
+
| VtNoProof of (unit -> unit)
- | VtCloseProof of (pstate:Proof_global.t -> unit)
- | VtOpenProof of (unit -> Proof_global.t)
+ | VtCloseProof of (lemma:Lemmas.t -> unit)
+ | VtOpenProof of (unit -> Lemmas.t)
| VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
| VtReadProofOpt of (pstate:Proof_global.t option -> unit)
| VtReadProof of (pstate:Proof_global.t -> unit)
@@ -129,9 +129,9 @@ let get_vernac_classifier (name, i) args =
let declare_vernac_classifier name f =
classifiers := String.Map.add name f !classifiers
-let classify_as_query = VtQuery, VtLater
-let classify_as_sideeff = VtSideff [], VtLater
-let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
+let classify_as_query = VtQuery
+let classify_as_sideeff = VtSideff ([], VtLater)
+let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}
type (_, _) ty_sig =
| TyNil : (vernac_command, vernac_classification) ty_sig
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 60e371a6d9..fd59d77237 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -32,7 +32,11 @@ type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque
type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop
-type vernac_type =
+type vernac_when =
+ | VtNow
+ | VtLater
+
+type vernac_classification =
(* Start of a proof *)
| VtStartProof of vernac_start
(* Command altering the global state, bad for parallel
@@ -53,7 +57,7 @@ type vernac_type =
(* To be removed *)
| VtMeta
and vernac_start = opacity_guarantee * Names.Id.t list
-and vernac_sideff_type = Names.Id.t list
+and vernac_sideff_type = Names.Id.t list * vernac_when
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
| Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
@@ -64,18 +68,13 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *)
and proof_block_name = string (** open type of delimiters *)
-type vernac_when =
- | VtNow
- | VtLater
-type vernac_classification = vernac_type * vernac_when
-
(** Interpretation of extended vernac phrases. *)
type typed_vernac =
| VtDefault of (unit -> unit)
| VtNoProof of (unit -> unit)
- | VtCloseProof of (pstate:Proof_global.t -> unit)
- | VtOpenProof of (unit -> Proof_global.t)
+ | VtCloseProof of (lemma:Lemmas.t -> unit)
+ | VtOpenProof of (unit -> Lemmas.t)
| VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
| VtReadProofOpt of (pstate:Proof_global.t option -> unit)
| VtReadProof of (pstate:Proof_global.t -> unit)
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 0fbde1ade5..c51d3c30f4 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -30,18 +30,16 @@ end
type t = {
parsing : Parser.state;
system : States.state; (* summary + libstack *)
- proof : Proof_global.stack option; (* proof state *)
+ lemmas : Lemmas.Stack.t option; (* proofs of lemmas currently opened *)
shallow : bool (* is the state trimmed down (libstack) *)
}
-let pstate st = Option.map Proof_global.get_current_pstate st.proof
-
let s_cache = ref None
-let s_proof = ref None
+let s_lemmas = ref None
let invalidate_cache () =
s_cache := None;
- s_proof := None
+ s_lemmas := None
let update_cache rf v =
rf := Some v; v
@@ -57,14 +55,14 @@ let do_if_not_cached rf f v =
let freeze_interp_state ~marshallable =
{ system = update_cache s_cache (States.freeze ~marshallable);
- proof = !s_proof;
+ lemmas = !s_lemmas;
shallow = false;
parsing = Parser.cur_state ();
}
-let unfreeze_interp_state { system; proof; parsing } =
+let unfreeze_interp_state { system; lemmas; parsing } =
do_if_not_cached s_cache States.unfreeze system;
- s_proof := proof;
+ s_lemmas := lemmas;
Pcoq.unfreeze parsing
let make_shallow st =
@@ -77,11 +75,16 @@ let make_shallow st =
(* Compatibility module *)
module Proof_global = struct
- let get () = !s_proof
- let set x = s_proof := x
+ type t = Lemmas.Stack.t
+
+ let get () = !s_lemmas
+ let set x = s_lemmas := x
+
+ let get_pstate () =
+ Option.map (Lemmas.Stack.with_top ~f:(Lemmas.pf_fold (fun x -> x))) !s_lemmas
let freeze ~marshallable:_ = get ()
- let unfreeze x = s_proof := Some x
+ let unfreeze x = s_lemmas := Some x
exception NoCurrentProof
@@ -92,53 +95,62 @@ module Proof_global = struct
| _ -> raise CErrors.Unhandled
end
+ open Lemmas
open Proof_global
- let cc f = match !s_proof with
+ let cc f = match !s_lemmas with
| None -> raise NoCurrentProof
- | Some x -> f x
-
- let cc1 f = cc (fun p -> f (Proof_global.get_current_pstate p))
+ | Some x -> Stack.with_top_pstate ~f x
- let dd f = match !s_proof with
+ let cc_lemma f = match !s_lemmas with
| None -> raise NoCurrentProof
- | Some x -> s_proof := Some (f x)
+ | Some x -> Stack.with_top ~f x
- let dd1 f = dd (fun p -> Proof_global.modify_current_pstate f p)
+ let cc_stack f = match !s_lemmas with
+ | None -> raise NoCurrentProof
+ | Some x -> f x
- let there_are_pending_proofs () = !s_proof <> None
- let get_open_goals () = cc1 get_open_goals
+ let dd f = match !s_lemmas with
+ | None -> raise NoCurrentProof
+ | Some x -> s_lemmas := Some (Stack.map_top_pstate ~f x)
- let set_terminator x = dd1 (set_terminator x)
- let give_me_the_proof_opt () = Option.map (fun p -> give_me_the_proof (Proof_global.get_current_pstate p)) !s_proof
- let give_me_the_proof () = cc1 give_me_the_proof
- let get_current_proof_name () = cc1 get_current_proof_name
+ let there_are_pending_proofs () = !s_lemmas <> None
+ let get_open_goals () = cc get_open_goals
- let simple_with_current_proof f =
- dd (simple_with_current_proof f)
+ let give_me_the_proof_opt () = Option.map (Stack.with_top_pstate ~f:get_proof) !s_lemmas
+ let give_me_the_proof () = cc get_proof
+ let get_current_proof_name () = cc get_proof_name
+ let map_proof f = dd (map_proof f)
let with_current_proof f =
- let pf, res = cc (with_current_proof f) in
- s_proof := Some pf; res
+ match !s_lemmas with
+ | None -> raise NoCurrentProof
+ | Some stack ->
+ let pf, res = Stack.with_top_pstate stack ~f:(map_fold_proof_endline f) in
+ let stack = Stack.map_top_pstate stack ~f:(fun _ -> pf) in
+ s_lemmas := Some stack;
+ res
+
+ type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator
- let install_state s = s_proof := Some s
- let return_proof ?allow_partial () =
- cc1 (return_proof ?allow_partial)
+ let return_proof ?allow_partial () = cc (return_proof ?allow_partial)
let close_future_proof ~opaque ~feedback_id pf =
- cc1 (fun st -> close_future_proof ~opaque ~feedback_id st pf)
+ cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt,
+ Internal.get_terminator pt)
let close_proof ~opaque ~keep_body_ucst_separate f =
- cc1 (close_proof ~opaque ~keep_body_ucst_separate f)
+ cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate f)) pt,
+ Internal.get_terminator pt)
- let discard_all () = s_proof := None
- let update_global_env () = dd1 update_global_env
+ let discard_all () = s_lemmas := None
+ let update_global_env () = dd (update_global_env)
- let get_current_context () = cc1 Pfedit.get_current_context
+ let get_current_context () = cc Pfedit.get_current_context
let get_all_proof_names () =
- try cc get_all_proof_names
+ try cc_stack Lemmas.Stack.get_all_proof_names
with NoCurrentProof -> []
let copy_terminators ~src ~tgt =
@@ -146,6 +158,6 @@ module Proof_global = struct
| None, None -> None
| Some _ , None -> None
| None, Some x -> Some x
- | Some src, Some tgt -> Some (copy_terminators ~src ~tgt)
+ | Some src, Some tgt -> Some (Stack.copy_terminators ~src ~tgt)
end
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index b0f3c572e5..9f4e366e1c 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -18,14 +18,12 @@ module Parser : sig
end
-type t = {
- parsing : Parser.state;
- system : States.state; (* summary + libstack *)
- proof : Proof_global.stack option; (* proof state *)
- shallow : bool (* is the state trimmed down (libstack) *)
-}
-
-val pstate : t -> Proof_global.t option
+type t =
+ { parsing : Parser.state
+ ; system : States.state (* summary + libstack *)
+ ; lemmas : Lemmas.Stack.t option (* proofs of lemmas currently opened *)
+ ; shallow : bool (* is the state trimmed down (libstack) *)
+ }
val freeze_interp_state : marshallable:bool -> t
val unfreeze_interp_state : t -> unit
@@ -38,41 +36,29 @@ val invalidate_cache : unit -> unit
(* Compatibility module: Do Not Use *)
module Proof_global : sig
- open Proof_global
-
- (* Low-level stuff *)
- val get : unit -> stack option
- val set : stack option -> unit
-
- val freeze : marshallable:bool -> stack option
- val unfreeze : stack -> unit
-
exception NoCurrentProof
val there_are_pending_proofs : unit -> bool
val get_open_goals : unit -> int
- val set_terminator : proof_terminator -> unit
val give_me_the_proof : unit -> Proof.t
val give_me_the_proof_opt : unit -> Proof.t option
val get_current_proof_name : unit -> Names.Id.t
- val simple_with_current_proof :
- (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit
-
+ val map_proof : (Proof.t -> Proof.t) -> unit
val with_current_proof :
(unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
- val install_state : stack -> unit
+ val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output
- val return_proof : ?allow_partial:bool -> unit -> closed_proof_output
+ type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator
val close_future_proof :
- opaque:opacity_flag ->
+ opaque:Proof_global.opacity_flag ->
feedback_id:Stateid.t ->
- closed_proof_output Future.computation -> closed_proof
+ Proof_global.closed_proof_output Future.computation -> closed_proof
- val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
+ val close_proof : opaque:Proof_global.opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
val discard_all : unit -> unit
val update_global_env : unit -> unit
@@ -81,7 +67,19 @@ module Proof_global : sig
val get_all_proof_names : unit -> Names.Id.t list
- val copy_terminators : src:stack option -> tgt:stack option -> stack option
+ val copy_terminators : src:Lemmas.Stack.t option -> tgt:Lemmas.Stack.t option -> Lemmas.Stack.t option
+
+ (* Handling of the imperative state *)
+ type t = Lemmas.Stack.t
+
+ (* Low-level stuff *)
+ val get : unit -> t option
+ val set : t option -> unit
+
+ val get_pstate : unit -> Proof_global.t option
+
+ val freeze : marshallable:bool -> t option
+ val unfreeze : t -> unit
end
[@@ocaml.deprecated "This module is internal and should not be used, instead, thread the proof state"]
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 17:42:50 +0000