aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml135
-rw-r--r--vernac/classes.mli14
-rw-r--r--vernac/comFixpoint.ml16
-rw-r--r--vernac/comFixpoint.mli12
-rw-r--r--vernac/lemmas.ml30
-rw-r--r--vernac/lemmas.mli21
-rw-r--r--vernac/obligations.ml14
-rw-r--r--vernac/obligations.mli10
-rw-r--r--vernac/search.mli12
-rw-r--r--vernac/vernacentries.ml88
-rw-r--r--vernac/vernacstate.ml24
11 files changed, 198 insertions, 178 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index ea66234993..c783531f91 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -309,7 +309,7 @@ let id_of_class cl =
mip.(0).Declarations.mind_typename
| _ -> assert false
-let instance_hook k info global imps ?hook cst =
+let instance_hook info global imps ?hook cst =
Impargs.maybe_declare_manual_implicits false cst imps;
let info = intern_info info in
let env = Global.env () in
@@ -317,7 +317,7 @@ let instance_hook k info global imps ?hook cst =
declare_instance env sigma (Some info) (not global) cst;
(match hook with Some h -> h cst | None -> ())
-let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
+let declare_instance_constant info global imps ?hook id decl poly sigma term termtype =
(* XXX: Duplication of the declare_constant path *)
let kind = IsDefinition Instance in
let sigma =
@@ -331,7 +331,7 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t
let kn = Declare.declare_constant id cdecl in
Declare.definition_message id;
Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
- instance_hook k info global imps ?hook (ConstRef kn)
+ instance_hook info global imps ?hook (ConstRef kn)
let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst id =
let subst = List.fold_left2
@@ -344,66 +344,65 @@ let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
(ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in
Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
- instance_hook k pri global imps (ConstRef cst)
+ instance_hook pri global imps (ConstRef cst)
-let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype =
+let declare_instance_program env sigma ~global ~poly id pri imps decl term termtype =
+ let hook _ _ vis gr =
+ let cst = match gr with ConstRef kn -> kn | _ -> assert false in
+ Impargs.declare_manual_implicits false gr imps;
+ let pri = intern_info pri in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ declare_instance env sigma (Some pri) (not global) (ConstRef cst)
+ in
+ let obls, constr, typ =
+ match term with
+ | Some t ->
+ let termtype = EConstr.of_constr termtype in
+ let obls, _, constr, typ =
+ Obligations.eterm_obligations env id sigma 0 t termtype
+ in obls, Some constr, typ
+ | None -> [||], None, termtype
+ in
+ 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)
+
+
+let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids term termtype =
+ (* spiwack: it is hard to reorder the actions to do
+ the pretyping after the proof has opened. As a
+ consequence, we use the low-level primitives to code
+ 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
- if program_mode then
- let hook _ _ vis gr =
- let cst = match gr with ConstRef kn -> kn | _ -> assert false in
- Impargs.declare_manual_implicits false gr imps;
- let pri = intern_info pri in
- let env = Global.env () in
- let sigma = Evd.from_env env in
- declare_instance env sigma (Some pri) (not global) (ConstRef cst)
- in
- let obls, constr, typ =
- match term with
- | Some t ->
- let termtype = EConstr.of_constr termtype in
- let obls, _, constr, typ =
- Obligations.eterm_obligations env id sigma 0 t termtype
- in obls, Some constr, typ
- | None -> [||], None, termtype
- in
- let hook = Lemmas.mk_hook hook in
- let ctx = Evd.evar_universe_context sigma in
- let _progress = Obligations.add_definition id ?term:constr
- ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls in
+ let pstate = Lemmas.start_proof 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 =
+ if not (Option.is_empty term) then
+ let init_refine =
+ Tacticals.New.tclTHENLIST [
+ Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term));
+ Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
+ Tactics.New.reduce_after_refine;
+ ]
+ in
+ let pstate, _ = Pfedit.by init_refine pstate in
+ pstate
+ else
+ let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in
+ pstate
+ in
+ match tac with
+ | Some tac ->
+ let pstate, _ = Pfedit.by tac pstate in
+ pstate
+ | None ->
pstate
- else
- Some Flags.(silently (fun () ->
- (* spiwack: it is hard to reorder the actions to do
- the pretyping after the proof has opened. As a
- consequence, we use the low-level primitives to code
- the refinement manually.*)
- let gls = List.rev (Evd.future_goals sigma) in
- let sigma = Evd.reset_future_goals sigma in
- let pstate = Lemmas.start_proof ~ontop:pstate id ~pl:decl kind sigma (EConstr.of_constr termtype)
- ~hook:(Lemmas.mk_hook
- (fun _ _ _ -> instance_hook k pri global imps ?hook)) in
- (* spiwack: I don't know what to do with the status here. *)
- let pstate =
- if not (Option.is_empty term) then
- let init_refine =
- Tacticals.New.tclTHENLIST [
- Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term));
- Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
- Tactics.New.reduce_after_refine;
- ]
- in
- let pstate, _ = Pfedit.by init_refine pstate in
- pstate
- else
- let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in
- pstate
- in
- match tac with
- | Some tac ->
- let pstate, _ = Pfedit.by tac pstate in
- pstate
- | None ->
- pstate) ())
let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
let props =
@@ -487,10 +486,18 @@ let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode ct
let pstate =
if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
let term = to_constr sigma (Option.get term) in
- (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype;
- None)
- else if program_mode || Option.is_empty props then
- declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
+ (declare_instance_constant pri global imps ?hook id decl poly sigma term termtype;
+ pstate)
+ else if program_mode then
+ (declare_instance_program env sigma ~global ~poly id pri imps decl term termtype ; pstate)
+ else if Option.is_empty props then
+ let pstate' =
+ Flags.silently (fun () ->
+ declare_instance_open sigma ?hook ~tac ~global ~poly
+ id pri imps decl (List.map RelDecl.get_name ctx) term termtype)
+ ()
+ in
+ Some (Proof_global.push ~ontop:pstate pstate')
else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in
id, pstate
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 8d5f3e3a06..f80dbb9897 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -31,20 +31,6 @@ 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 declare_instance_constant :
- typeclass ->
- Hints.hint_info_expr (** priority *) ->
- bool (** globality *) ->
- Impargs.manual_explicitation list (** implicits *) ->
- ?hook:(GlobRef.t -> unit) ->
- Id.t (** name *) ->
- UState.universe_decl ->
- bool (** polymorphic *) ->
- Evd.evar_map (** Universes *) ->
- Constr.t (** body *) ->
- Constr.types (** type *) ->
- unit
-
val new_instance :
pstate:Proof_global.t option
-> ?global:bool (** Not global by default. *)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a428c42e49..006ac314a5 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -255,7 +255,7 @@ let interp_fixpoint ~cofix l ntns =
let uctx,fix = ground_fixpoint env evd fix in
(fix,pl,uctx,info)
-let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
let pstate =
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
@@ -267,7 +267,7 @@ let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx
fixdefs) in
let evd = Evd.from_ctx ctx in
Some
- (Lemmas.start_proof_with_initialization ~ontop (local,poly,DefinitionBody Fixpoint)
+ (Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint)
evd pl (Some(false,indexes,init_tac)) thms None)
else begin
(* We shortcut the proof process *)
@@ -294,7 +294,7 @@ let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx
List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
pstate
-let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
let pstate =
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
@@ -305,7 +305,7 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
fixdefs) in
let evd = Evd.from_ctx ctx in
- Some (Lemmas.start_proof_with_initialization ~ontop (Global,poly, DefinitionBody CoFixpoint)
+ Some (Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
evd pl (Some(true,[],init_tac)) thms None)
else begin
(* We shortcut the proof process *)
@@ -366,18 +366,18 @@ let check_safe () =
let flags = Environ.typing_flags (Global.env ()) in
flags.check_universes && flags.check_guarded
-let do_fixpoint ~ontop local poly l =
+let do_fixpoint local poly l =
let fixl, ntns = extract_fixpoint_components ~structonly:true l in
let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
let possible_indexes =
List.map compute_possible_guardness_evidences info in
- let pstate = declare_fixpoint ~ontop local poly fix possible_indexes ntns in
+ let pstate = declare_fixpoint local poly fix possible_indexes ntns in
if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
pstate
-let do_cofixpoint ~ontop local poly l =
+let do_cofixpoint local poly l =
let fixl,ntns = extract_cofixpoint_components l in
let cofix = interp_fixpoint ~cofix:true fixl ntns in
- let pstate = declare_cofixpoint ~ontop local poly cofix ntns in
+ let pstate = declare_cofixpoint local poly cofix ntns in
if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
pstate
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 5937842f17..d36593332e 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -19,14 +19,12 @@ open Vernacexpr
(** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
val do_fixpoint :
- ontop:Proof_global.t option ->
(* When [false], assume guarded. *)
- locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t option
+ locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.pstate option
val do_cofixpoint :
- ontop:Proof_global.t option ->
(* When [false], assume guarded. *)
- locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t option
+ locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.pstate option
(************************************************************************)
(** Internal API *)
@@ -83,20 +81,18 @@ val interp_fixpoint :
(** [Not used so far] *)
val declare_fixpoint :
- ontop:Proof_global.t option ->
locality -> polymorphic ->
recursive_preentry * UState.universe_decl * UState.t *
(Constr.rel_context * Impargs.manual_implicits * int option) list ->
Proof_global.lemma_possible_guards -> decl_notation list ->
- Proof_global.t option
+ Proof_global.pstate option
val declare_cofixpoint :
- ontop:Proof_global.t option ->
locality -> polymorphic ->
recursive_preentry * UState.universe_decl * UState.t *
(Constr.rel_context * Impargs.manual_implicits * int option) list ->
decl_notation list ->
- Proof_global.t option
+ Proof_global.pstate option
(** Very private function, do not use *)
val compute_possible_guardness_evidences :
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 740b9031cc..d0ec575eb3 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -329,7 +329,7 @@ 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 ~ontop id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
+let start_proof 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
@@ -340,7 +340,7 @@ let start_proof ~ontop id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?
| None -> initialize_named_context_for_proof ()
in
let goals = [ Global.env_of_context sign , c ] in
- Proof_global.start_proof ~ontop sigma id ?pl kind goals terminator
+ Proof_global.start_proof sigma id ?pl kind goals terminator
let rec_tac_initializer finite guard thms snl =
if finite then
@@ -356,7 +356,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 ~ontop ?hook kind sigma decl recguard thms snl =
+let start_proof_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) ->
@@ -388,14 +388,14 @@ let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms s
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
call_hook ?hook ctx [] strength ref) thms_data in
- let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
- let pstate = Proof_global.simple_with_current_proof (fun _ p ->
+ let pstate = start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
+ let pstate = Proof_global.modify_proof (fun p ->
match init_tac with
| None -> p
| Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in
pstate
-let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms =
+let start_proof_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
@@ -427,7 +427,7 @@ let start_proof_com ~program_mode ~ontop ?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 ~ontop ?hook kind evd decl recguard thms snl
+ start_proof_with_initialization ?hook kind evd decl recguard thms snl
(* Saving a proof *)
@@ -487,20 +487,26 @@ let save_proof_admitted ?proof ~pstate =
in
Proof_global.apply_terminator (Proof_global.get_terminator pstate) pe
-let save_proof_proved ?proof ?pstate ~opaque ~idopt =
+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)))
+
+let save_proof_proved ?proof ?ontop ~opaque ~idopt =
(* Invariant (uh) *)
- if Option.is_empty pstate && Option.is_empty proof then
+ if Option.is_empty ontop && 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 = Option.get pstate in
+ 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
| Some proof -> proof
in
(* if the proof is given explicitly, nothing has to be deleted *)
- let pstate = if Option.is_empty proof then Proof_global.discard_current Option.(get pstate) else pstate in
+ 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)));
- pstate
+ ontop
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 1f70cfa1ad..ad6eb024aa 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -37,26 +37,25 @@ val call_hook
-> ?fix_exn:Future.fix_exn
-> hook_type
-val start_proof : ontop:Proof_global.t option -> Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
+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
+ ?hook:declaration_hook -> EConstr.types -> Proof_global.pstate
val start_proof_com
: program_mode:bool
- -> ontop:Proof_global.t option
-> ?inference_hook:Pretyping.inference_hook
-> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list
- -> Proof_global.t
+ -> Proof_global.pstate
-val start_proof_with_initialization : ontop:Proof_global.t option ->
+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
+ -> int list option -> Proof_global.pstate
val standard_proof_terminator :
?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
@@ -73,12 +72,18 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
val save_proof_admitted
: ?proof:Proof_global.closed_proof
- -> pstate:Proof_global.t
+ -> pstate:Proof_global.pstate
-> unit
val save_proof_proved
: ?proof:Proof_global.closed_proof
- -> ?pstate:Proof_global.t
+ -> ?ontop:Proof_global.t
-> opaque:Proof_global.opacity_flag
-> idopt:Names.lident option
-> Proof_global.t option
+
+val save_pstate_proved
+ : pstate:Proof_global.pstate
+ -> opaque:Proof_global.opacity_flag
+ -> idopt:Names.lident option
+ -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index bc741a0ec7..0d93e19723 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -760,7 +760,7 @@ let update_obls prg obls rem =
match prg'.prg_deps with
| [] ->
let kn = declare_definition prg' in
- progmap_remove prg';
+ progmap_remove prg';
Defined kn
| l ->
let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in
@@ -944,7 +944,7 @@ let obligation_hook prg obl num auto ctx' _ _ gr =
ignore (auto (Some prg.prg_name) None deps)
end
-let rec solve_obligation ~ontop prg num tac =
+let rec solve_obligation prg num tac =
let user_num = succ num in
let obls, rem = prg.prg_obligations in
let obl = obls.(num) in
@@ -965,19 +965,19 @@ let rec solve_obligation ~ontop prg num tac =
Proof_global.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 ~ontop ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook 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
-and obligation ~ontop (user_num, name, typ) tac =
+and obligation (user_num, name, typ) tac =
let num = pred user_num in
let prg = get_prog_err name in
let obls, rem = prg.prg_obligations in
if num >= 0 && num < Array.length obls then
let obl = obls.(num) in
match obl.obl_body with
- | None -> solve_obligation ~ontop prg num tac
+ | None -> solve_obligation prg num tac
| Some r -> error "Obligation already solved"
else error (sprintf "Unknown obligation number %i" (succ num))
@@ -1177,7 +1177,7 @@ let admit_obligations n =
let prg = get_prog_err n in
admit_prog prg
-let next_obligation ~ontop n tac =
+let next_obligation n tac =
let prg = match n with
| None -> get_any_prog_err ()
| Some _ -> get_prog_err n
@@ -1188,7 +1188,7 @@ let next_obligation ~ontop n tac =
| Some i -> i
| None -> anomaly (Pp.str "Could not find a solvable obligation.")
in
- solve_obligation ~ontop prg i tac
+ solve_obligation prg i tac
let check_program_libraries () =
Coqlib.check_required_library Coqlib.datatypes_module_name;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 9214ddd4b9..7db094a75d 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -86,16 +86,14 @@ val add_mutual_definitions :
fixpoint_kind -> unit
val obligation
- : ontop:Proof_global.t option
- -> 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
+ -> Proof_global.pstate
val next_obligation
- : ontop:Proof_global.t option
- -> Names.Id.t option
+ : Names.Id.t option
-> Genarg.glob_generic_argument option
- -> Proof_global.t
+ -> Proof_global.pstate
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/search.mli b/vernac/search.mli
index 0f94ddc5b6..f8074a67ff 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -39,13 +39,13 @@ val search_about_filter : glob_search_about_item -> filter_function
goal and the global environment for things matching [pattern] and
satisfying module exclude/include clauses of [modinout]. *)
-val search_by_head : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_by_head : ?pstate:Proof_global.pstate -> int option -> constr_pattern -> DirPath.t list * bool
-> display_function -> unit
-val search_rewrite : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_rewrite : ?pstate:Proof_global.pstate -> int option -> constr_pattern -> DirPath.t list * bool
-> display_function -> unit
-val search_pattern : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_pattern : ?pstate:Proof_global.pstate -> int option -> constr_pattern -> DirPath.t list * bool
-> display_function -> unit
-val search_about : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list
+val search_about : ?pstate:Proof_global.pstate -> int option -> (bool * glob_search_about_item) list
-> DirPath.t list * bool -> display_function -> unit
type search_constraint =
@@ -66,12 +66,12 @@ type 'a coq_object = {
coq_object_object : 'a;
}
-val interface_search : ?pstate:Proof_global.t -> ?glnum:int -> (search_constraint * bool) list ->
+val interface_search : ?pstate:Proof_global.pstate -> ?glnum:int -> (search_constraint * bool) list ->
constr coq_object list
(** {6 Generic search function} *)
-val generic_search : ?pstate:Proof_global.t -> int option -> display_function -> unit
+val generic_search : ?pstate:Proof_global.pstate -> int option -> display_function -> unit
(** This function iterates over all hypothesis of the goal numbered
[glnum] (if present) and all known declarations. *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 337cb233a2..f92c1f9c27 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -56,6 +56,10 @@ let vernac_require_open_proof ~pstate f =
| Some pstate -> f ~pstate
| 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 get_current_or_global_context ~pstate =
match pstate with
| None -> let env = Global.env () in Evd.(from_env env, env)
@@ -540,7 +544,7 @@ let () =
(***********)
(* Gallina *)
-let start_proof_and_print ~program_mode ~pstate ?hook k l =
+let start_proof_and_print ~program_mode ?hook k l =
let inference_hook =
if program_mode then
let hook env sigma ev =
@@ -562,7 +566,7 @@ let start_proof_and_print ~program_mode ~pstate ?hook k l =
in Some hook
else None
in
- start_proof_com ~program_mode ~ontop:pstate ?inference_hook ?hook k l
+ start_proof_com ~program_mode ?inference_hook ?hook k l
let vernac_definition_hook p = function
| Coercion ->
@@ -573,7 +577,7 @@ let vernac_definition_hook p = function
Some (Class.add_subclass_hook p)
| _ -> None
-let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def =
+let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def ~pstate =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
let hook = vernac_definition_hook atts.polymorphic kind in
@@ -593,9 +597,10 @@ let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def =
in
(match def with
| ProveBody (bl,t) -> (* local binders, typ *)
- Some (start_proof_and_print ~program_mode ~pstate (local, atts.polymorphic, DefinitionBody kind)
+ Some (start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind)
?hook [(CAst.make ?loc name, pl), (bl, t)])
| DefineBody (bl,red_option,c,typ_opt) ->
+ let pstate = Option.map Proof_global.get_current_pstate pstate in
let red_option = match red_option with
| None -> None
| Some r ->
@@ -603,30 +608,31 @@ let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def =
Some (snd (Hook.get f_interp_redexp env sigma r)) in
ComDefinition.do_definition ~program_mode name
(local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook;
- pstate
+ None
)
-let vernac_start_proof ~atts ~pstate kind l =
+(* NB: pstate argument to use combinators easily *)
+let vernac_start_proof ~atts kind l ~pstate =
let open DefAttributes in
let local = enforce_locality_exp atts.locality NoDischarge in
if Dumpglob.dump () then
List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
- Some (start_proof_and_print ~pstate ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l)
+ Some (start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l)
-let vernac_end_proof ?pstate ?proof = function
+let vernac_end_proof ?pstate:ontop ?proof = function
| Admitted ->
- vernac_require_open_proof ~pstate (save_proof_admitted ?proof);
- pstate
+ with_pstate ~pstate:ontop (save_proof_admitted ?proof);
+ ontop
| Proved (opaque,idopt) ->
- save_proof_proved ?pstate ?proof ~opaque ~idopt
+ save_proof_proved ?ontop ?proof ~opaque ~idopt
-let vernac_exact_proof ~pstate c =
+let vernac_exact_proof ~pstate:ontop 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 pstate = save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Opaque ~idopt:None in
+ let pstate, status = Pfedit.by (Tactics.exact_proof c) (Proof_global.get_current_pstate ontop) in
+ let () = save_pstate_proved ~pstate ~opaque:Proof_global.Opaque ~idopt:None in
if not status then Feedback.feedback Feedback.AddedAxiom;
- pstate
+ Proof_global.discard_current ontop
let vernac_assumption ~atts discharge kind l nl =
let open DefAttributes in
@@ -804,7 +810,7 @@ let vernac_inductive ~atts cum lo finite indl =
in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
*)
-let vernac_fixpoint ~atts ~pstate discharge l : Proof_global.t option =
+let vernac_fixpoint ~atts discharge l ~pstate =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
if Dumpglob.dump () then
@@ -813,11 +819,11 @@ let vernac_fixpoint ~atts ~pstate discharge l : Proof_global.t option =
let do_fixpoint = if atts.program then
fun local sign l -> ComProgramFixpoint.do_fixpoint local sign l; None
else
- ComFixpoint.do_fixpoint ~ontop:pstate
+ ComFixpoint.do_fixpoint
in
do_fixpoint local atts.polymorphic l
-let vernac_cofixpoint ~atts ~pstate discharge l =
+let vernac_cofixpoint ~atts discharge l ~pstate =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
if Dumpglob.dump () then
@@ -825,7 +831,7 @@ let vernac_cofixpoint ~atts ~pstate discharge l =
let do_cofixpoint = if atts.program then
fun local sign l -> ComProgramFixpoint.do_cofixpoint local sign l; None
else
- ComFixpoint.do_cofixpoint ~ontop:pstate
+ ComFixpoint.do_cofixpoint
in
do_cofixpoint local atts.polymorphic l
@@ -1104,7 +1110,7 @@ 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 : Proof_global.pstate) e : Proof_global.pstate =
let env = Global.env () in
let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
let tys =
@@ -1118,9 +1124,7 @@ let vernac_set_used_variables ~(pstate : Proof_global.t) e : Proof_global.t =
(str "Unknown variable: " ++ Id.print id))
l;
let _, pstate = Proof_global.set_used_variables pstate l in
- fst @@ Proof_global.with_current_proof begin fun _ p ->
- (p, ())
- end pstate
+ pstate
(*****************************)
(* Auxiliary file management *)
@@ -1829,6 +1833,7 @@ let query_command_selector ?loc = function
(str "Query commands only support the single numbered goal selector.")
let vernac_check_may_eval ~pstate ~atts redexp glopt rc =
+ let pstate = Option.map Proof_global.get_current_pstate pstate in
let glopt = query_command_selector glopt in
let sigma, env = get_current_context_of_args ~pstate glopt in
let sigma, c = interp_open_constr env sigma rc in
@@ -1929,6 +1934,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
print_about env sigma ref_or_by_not udecl
let vernac_print ~(pstate : Proof_global.t option) ~atts =
+ let pstate = Option.map Proof_global.get_current_pstate pstate in
let sigma, env = get_current_or_global_context ~pstate in
function
| PrintTables -> print_tables ()
@@ -2040,6 +2046,7 @@ let () =
optwrite = (:=) search_output_name_only }
let vernac_search ~pstate ~atts s gopt r =
+ let pstate = Option.map Proof_global.get_current_pstate pstate in
let gopt = query_command_selector gopt in
let r = interp_search_restriction r in
let env,gopt =
@@ -2077,6 +2084,7 @@ let vernac_locate ~pstate = function
| LocateTerm {v=AN qid} -> print_located_term qid
| LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *)
| LocateTerm {v=ByNotation (ntn, sc)} ->
+ let pstate = Option.map Proof_global.get_current_pstate pstate in
let _, env = get_current_or_global_context ~pstate in
Notation.locate_notation
(Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc
@@ -2132,6 +2140,7 @@ let vernac_unfocus () =
(* Checks that a proof is fully unfocused. Raises an error if not. *)
let vernac_unfocused ~pstate =
+ let pstate = Proof_global.get_current_pstate pstate in
let p = Proof_global.give_me_the_proof pstate in
if Proof.unfocused p then
str"The proof is indeed fully unfocused."
@@ -2162,18 +2171,19 @@ let vernac_bullet (bullet : Proof_bullet.t) =
Proof_global.simple_with_current_proof (fun _ p ->
Proof_bullet.put p bullet)
-let vernac_show ~pstate =
- match pstate with
+let vernac_show ~pstate:ontop =
+ match ontop with
(* Show functions that don't require a proof state *)
| None ->
begin function
- | ShowProof -> show_proof ~pstate
+ | ShowProof -> show_proof ~pstate:None
| ShowMatch id -> show_match id
| _ ->
user_err (str "This command requires an open proof.")
end
(* Show functions that require a proof state *)
- | Some pstate ->
+ | Some ontop ->
+ let pstate = Proof_global.get_current_pstate ontop in
begin function
| ShowGoal goalref ->
let proof = Proof_global.give_me_the_proof pstate in
@@ -2185,7 +2195,7 @@ let vernac_show ~pstate =
| ShowExistentials -> show_top_evars ~pstate
| ShowUniverses -> show_universes ~pstate
| ShowProofNames ->
- pr_sequence Id.print (Proof_global.get_all_proof_names pstate)
+ pr_sequence Id.print (Proof_global.get_all_proof_names ontop)
| ShowIntros all -> show_intro ~pstate all
| ShowProof -> show_proof ~pstate:(Some pstate)
| ShowMatch id -> show_match id
@@ -2223,6 +2233,10 @@ let with_def_attributes ~atts f =
if atts.DefAttributes.program then Obligations.check_program_libraries ();
f ~atts
+let with_maybe_open_proof ~pstate f =
+ let opt = f ~pstate in
+ Proof_global.maybe_push ~ontop:pstate opt
+
(** A global default timeout, controlled by option "Set Default Timeout n".
Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
@@ -2339,9 +2353,9 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
(* Gallina *)
| VernacDefinition ((discharge,kind),lid,d) ->
- with_def_attributes ~atts vernac_definition ~pstate discharge kind lid d
+ with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_definition discharge kind lid d)
| VernacStartTheoremProof (k,l) ->
- with_def_attributes ~atts vernac_start_proof ~pstate k l
+ with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_start_proof k l)
| VernacEndProof e ->
unsupported_attributes atts;
vernac_end_proof ?proof ?pstate e
@@ -2355,9 +2369,9 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
vernac_inductive ~atts cum priv finite l;
pstate
| VernacFixpoint (discharge, l) ->
- with_def_attributes ~atts vernac_fixpoint ~pstate discharge l
+ with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_fixpoint discharge l)
| VernacCoFixpoint (discharge, l) ->
- with_def_attributes ~atts vernac_cofixpoint ~pstate discharge l
+ with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_cofixpoint discharge l)
| VernacScheme l ->
unsupported_attributes atts;
vernac_scheme l;
@@ -2587,7 +2601,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
| VernacCheckGuard ->
unsupported_attributes atts;
Feedback.msg_notice @@
- vernac_require_open_proof ~pstate (vernac_check_guard);
+ with_pstate ~pstate (vernac_check_guard);
pstate
| VernacProof (tac, using) ->
unsupported_attributes atts;
@@ -2596,10 +2610,14 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
let usings = if Option.is_empty using then "using:no" else "using:yes" in
Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings);
let pstate =
- vernac_require_open_proof ~pstate (fun ~pstate ->
+ vernac_require_open_proof ~pstate (fun ~pstate:ontop ->
+ Proof_global.modify_current_pstate (fun pstate ->
+ let pstate = Proof_global.get_current_pstate ontop in
let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in
Option.cata (vernac_set_used_variables ~pstate) pstate using)
- in Some pstate
+ ontop)
+ in
+ Some pstate
| VernacProofMode mn ->
unsupported_attributes atts;
pstate
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 77f54361da..9ab2d00fc2 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -96,17 +96,21 @@ module Proof_global = struct
| None -> raise NoCurrentProof
| Some x -> f x
+ let cc1 f = cc (fun p -> f (Proof_global.get_current_pstate p))
+
let dd f = match !s_proof with
| None -> raise NoCurrentProof
| Some x -> s_proof := Some (f x)
+ let dd1 f = dd (fun p -> Proof_global.modify_current_pstate f p)
+
let there_are_pending_proofs () = !s_proof <> None
- let get_open_goals () = cc get_open_goals
+ let get_open_goals () = cc1 get_open_goals
- let set_terminator x = dd (set_terminator x)
- let give_me_the_proof_opt () = Option.map give_me_the_proof !s_proof
- let give_me_the_proof () = cc give_me_the_proof
- let get_current_proof_name () = cc get_current_proof_name
+ 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 simple_with_current_proof f =
dd (simple_with_current_proof f)
@@ -118,18 +122,18 @@ module Proof_global = struct
let install_state s = s_proof := Some s
let return_proof ?allow_partial () =
- cc (return_proof ?allow_partial)
+ cc1 (return_proof ?allow_partial)
let close_future_proof ~opaque ~feedback_id pf =
- cc (fun st -> close_future_proof ~opaque ~feedback_id st pf)
+ cc1 (fun st -> close_future_proof ~opaque ~feedback_id st pf)
let close_proof ~opaque ~keep_body_ucst_separate f =
- cc (close_proof ~opaque ~keep_body_ucst_separate f)
+ cc1 (close_proof ~opaque ~keep_body_ucst_separate f)
let discard_all () = s_proof := None
- let update_global_env () = dd update_global_env
+ let update_global_env () = dd1 update_global_env
- let get_current_context () = cc Pfedit.get_current_context
+ let get_current_context () = cc1 Pfedit.get_current_context
let get_all_proof_names () =
try cc get_all_proof_names
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 02:00:43 +0000