aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/top_printers.ml12
-rw-r--r--ide/idetop.ml21
-rw-r--r--stm/proofBlockDelimiter.ml13
-rw-r--r--stm/stm.ml71
-rw-r--r--toplevel/ccompile.ml2
-rw-r--r--toplevel/coqc.ml3
-rw-r--r--toplevel/coqloop.ml6
-rw-r--r--toplevel/vernac.ml2
-rw-r--r--vernac/classes.ml69
-rw-r--r--vernac/classes.mli6
-rw-r--r--vernac/comAssumption.ml11
-rw-r--r--vernac/comDefinition.ml4
-rw-r--r--vernac/comDefinition.mli17
-rw-r--r--vernac/comFixpoint.ml47
-rw-r--r--vernac/comFixpoint.mli17
-rw-r--r--vernac/declareDef.ml8
-rw-r--r--vernac/declareDef.mli6
-rw-r--r--vernac/lemmas.ml52
-rw-r--r--vernac/lemmas.mli24
-rw-r--r--vernac/obligations.ml45
-rw-r--r--vernac/obligations.mli6
-rw-r--r--vernac/search.ml33
-rw-r--r--vernac/search.mli12
-rw-r--r--vernac/vernacentries.ml748
-rw-r--r--vernac/vernacentries.mli5
-rw-r--r--vernac/vernacstate.ml86
-rw-r--r--vernac/vernacstate.mli60
27 files changed, 904 insertions, 482 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 499bbba37e..1f4f2246be 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -60,19 +60,21 @@ let prrecarg = function
str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
let ppwf_paths x = pp (Rtree.pp_tree prrecarg x)
+let get_current_context = Vernacstate.Proof_global.get_current_context
+
(* term printers *)
-let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma
+let envpp pp = let sigma,env = get_current_context () in pp env sigma
let rawdebug = ref false
let ppevar evk = pp (Evar.print evk)
let pr_constr t =
- let sigma, env = Pfedit.get_current_context () in
+ let sigma, env = get_current_context () in
Printer.pr_constr_env env sigma t
let pr_econstr t =
- let sigma, env = Pfedit.get_current_context () in
+ let sigma, env = get_current_context () in
Printer.pr_econstr_env env sigma t
let ppconstr x = pp (pr_constr x)
let ppeconstr x = pp (pr_econstr x)
-let ppconstr_expr x = let sigma,env = Pfedit.get_current_context () in pp (Ppconstr.pr_constr_expr env sigma x)
+let ppconstr_expr x = let sigma,env = get_current_context () in pp (Ppconstr.pr_constr_expr env sigma x)
let ppsconstr x = ppconstr (Mod_subst.force_constr x)
let ppconstr_univ x = Constrextern.with_universes ppconstr x
let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x))
@@ -500,7 +502,7 @@ let ppist ist =
(* Vernac-level debugging commands *)
let in_current_context f c =
- let (evmap,sign) = Pfedit.get_current_context () in
+ let (evmap,sign) = get_current_context () in
f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*)
(* We expand the result of preprocessing to be independent of camlp5
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 608577b297..f744ce2ee3 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -231,30 +231,30 @@ let goals () =
let doc = get_doc () in
set_doc @@ Stm.finish ~doc;
try
- let newp = Proof_global.give_me_the_proof () in
+ let newp = Vernacstate.Proof_global.give_me_the_proof () in
if Proof_diffs.show_diffs () then begin
let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
let diff_goal_map = Proof_diffs.make_goal_map oldp newp in
Some (export_pre_goals Proof.(data newp) (process_goal_diffs diff_goal_map oldp))
end else
Some (export_pre_goals Proof.(data newp) process_goal)
- with Proof_global.NoCurrentProof -> None;;
+ with Vernacstate.Proof_global.NoCurrentProof -> None;;
let evars () =
try
let doc = get_doc () in
set_doc @@ Stm.finish ~doc;
- let pfts = Proof_global.give_me_the_proof () in
+ let pfts = Vernacstate.Proof_global.give_me_the_proof () in
let Proof.{ sigma } = Proof.data pfts in
let exl = Evar.Map.bindings (Evd.undefined_map sigma) in
let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in
let el = List.map map_evar exl in
Some el
- with Proof_global.NoCurrentProof -> None
+ with Vernacstate.Proof_global.NoCurrentProof -> None
let hints () =
try
- let pfts = Proof_global.give_me_the_proof () in
+ let pfts = Vernacstate.Proof_global.give_me_the_proof () in
let Proof.{ goals; sigma } = Proof.data pfts in
match goals with
| [] -> None
@@ -263,7 +263,7 @@ let hints () =
let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in
let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in
Some (hint_hyps, concl_next_tac)
- with Proof_global.NoCurrentProof -> None
+ with Vernacstate.Proof_global.NoCurrentProof -> None
(** Other API calls *)
@@ -284,11 +284,11 @@ let status force =
List.rev_map Names.Id.to_string l
in
let proof =
- try Some (Names.Id.to_string (Proof_global.get_current_proof_name ()))
- with Proof_global.NoCurrentProof -> None
+ try Some (Names.Id.to_string (Vernacstate.Proof_global.get_current_proof_name ()))
+ with Vernacstate.Proof_global.NoCurrentProof -> None
in
let allproofs =
- let l = Proof_global.get_all_proof_names () in
+ let l = Vernacstate.Proof_global.get_all_proof_names () in
List.map Names.Id.to_string l
in
{
@@ -336,7 +336,8 @@ let import_search_constraint = function
| Interface.Include_Blacklist -> Search.Include_Blacklist
let search flags =
- List.map export_coq_object (Search.interface_search (
+ let pstate = Vernacstate.Proof_global.get () in
+ List.map export_coq_object (Search.interface_search ?pstate (
List.map (fun (c, b) -> (import_search_constraint c, b)) flags)
)
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 230a3207a8..d13763cdec 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -49,12 +49,13 @@ let is_focused_goal_simple ~doc id =
match state_of_id ~doc id with
| `Expired | `Error _ | `Valid None -> `Not
| `Valid (Some { Vernacstate.proof }) ->
- let proof = Proof_global.proof_of_state proof in
- let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in
- let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
- if List.for_all (fun x -> simple_goal sigma x rest) focused
- then `Simple focused
- else `Not
+ Option.cata (fun proof ->
+ let proof = Proof_global.give_me_the_proof proof in
+ let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in
+ let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
+ if List.for_all (fun x -> simple_goal sigma x rest) focused
+ then `Simple focused
+ else `Not) `Not proof
type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
diff --git a/stm/stm.ml b/stm/stm.ml
index 0c5d0c7b5d..c11f8d86e6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -139,8 +139,8 @@ let may_pierce_opaque = function
| _ -> false
let update_global_env () =
- if Proof_global.there_are_pending_proofs () then
- Proof_global.update_global_env ()
+ if Vernacstate.Proof_global.there_are_pending_proofs () then
+ Vernacstate.Proof_global.update_global_env ()
module Vcs_ = Vcs.Make(Stateid.Self)
type future_proof = Proof_global.closed_proof_output Future.computation
@@ -872,7 +872,7 @@ end = struct (* {{{ *)
let invalidate_cur_state () = cur_id := Stateid.dummy
type proof_part =
- Proof_global.t *
+ Proof_global.t option *
int * (* Evarutil.meta_counter_summary_tag *)
int * (* Evd.evar_counter_summary_tag *)
Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
@@ -948,8 +948,8 @@ end = struct (* {{{ *)
let prev = (VCS.visit id).next in
if is_cached_and_valid prev
then { s with proof =
- Proof_global.copy_terminators
- ~src:(get_cached prev).proof ~tgt:s.proof }
+ Vernacstate.Proof_global.copy_terminators
+ ~src:((get_cached prev).proof) ~tgt:s.proof }
else s
with VCS.Expired -> s in
VCS.set_state id (FullState s)
@@ -957,7 +957,7 @@ end = struct (* {{{ *)
if is_cached_and_valid ontop then
let s = get_cached ontop in
let s = { s with proof =
- Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
+ Vernacstate.Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
let s = { s with system =
States.replace_summary s.system
begin
@@ -1009,8 +1009,8 @@ end = struct (* {{{ *)
if feedback_processed then
Hooks.(call state_computed ~doc id ~in_cache:false);
VCS.reached id;
- if Proof_global.there_are_pending_proofs () then
- VCS.goals id (Proof_global.get_open_goals ())
+ if Vernacstate.Proof_global.there_are_pending_proofs () then
+ VCS.goals id (Vernacstate.Proof_global.get_open_goals ())
with e ->
let (e, info) = CErrors.push e in
let good_id = !cur_id in
@@ -1130,9 +1130,9 @@ let show_script ?proof () =
try
let prf =
try match proof with
- | None -> Some (Proof_global.get_current_proof_name ())
+ | None -> Some (Vernacstate.Proof_global.get_current_proof_name ())
| Some (p,_) -> Some (p.Proof_global.id)
- with Proof_global.NoCurrentProof -> None
+ with Vernacstate.Proof_global.NoCurrentProof -> None
in
let cmds = get_script prf in
let _,_,_,indented_cmds =
@@ -1255,9 +1255,8 @@ end = struct (* {{{ *)
if Int.equal n 0 then `Stop id else `Cont (n-value)
let get_proof ~doc id =
- let open Vernacstate in
match state_of_id ~doc id with
- | `Valid (Some vstate) -> Some (Proof_global.proof_of_state vstate.proof)
+ | `Valid (Some vstate) -> Option.map Proof_global.give_me_the_proof vstate.Vernacstate.proof
| _ -> None
let undo_vernac_classifier v ~doc =
@@ -1296,7 +1295,7 @@ end = struct (* {{{ *)
| Some vcs, _ -> vcs in
let cb, _ =
try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs)
- with Failure _ -> raise Proof_global.NoCurrentProof in
+ with Failure _ -> raise Vernacstate.Proof_global.NoCurrentProof in
let n = fold_until (fun n (_,vcs,_,_,_) ->
if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n)
0 id in
@@ -1334,7 +1333,7 @@ end = struct (* {{{ *)
| None -> true
done;
!rv
- with Not_found | Proof_global.NoCurrentProof -> None
+ with Not_found | Vernacstate.Proof_global.NoCurrentProof -> None
end (* }}} *)
@@ -1595,7 +1594,7 @@ end = struct (* {{{ *)
let wall_clock2 = Unix.gettimeofday () in
Aux_file.record_in_aux_at ?loc "proof_build_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
- let p = Proof_global.return_proof ~allow_partial:drop_pt () in
+ let p = Vernacstate.Proof_global.return_proof ~allow_partial:drop_pt () in
if drop_pt then feedback ~id Complete;
p)
@@ -1622,7 +1621,7 @@ end = struct (* {{{ *)
to set the state manually here *)
State.unfreeze st;
let pobject, _ =
- Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in
+ Vernacstate.Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in
let terminator = (* The one sent by master is an InvalidKey *)
Lemmas.(standard_proof_terminator []) in
@@ -1759,15 +1758,15 @@ end = struct (* {{{ *)
try
Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop;
if drop then
- let _proof = Proof_global.return_proof ~allow_partial:true () in
+ let _proof = Vernacstate.Proof_global.return_proof ~allow_partial:true () in
`OK_ADMITTED
else begin
(* The original terminator, a hook, has not been saved in the .vio*)
- Proof_global.set_terminator (Lemmas.standard_proof_terminator []);
+ Vernacstate.Proof_global.set_terminator (Lemmas.standard_proof_terminator []);
let opaque = Proof_global.Opaque in
let proof =
- Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
+ Vernacstate.Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
(* We jump at the beginning since the kernel handles side effects by also
* looking at the ones that happen to be present in the current env *)
Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false start;
@@ -2017,7 +2016,7 @@ end = struct (* {{{ *)
try
Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:false id;
State.purify (fun () ->
- let Proof.{sigma=sigma0} = Proof.data (Proof_global.give_me_the_proof ()) in
+ let Proof.{sigma=sigma0} = Proof.data (Vernacstate.Proof_global.give_me_the_proof ()) in
let g = Evd.find sigma0 r_goal in
let is_ground c = Evarutil.is_ground_term sigma0 c in
if not (
@@ -2029,7 +2028,7 @@ end = struct (* {{{ *)
"goals only"))
else begin
let (i, ast) = r_ast in
- Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
+ Vernacstate.Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
(* STATE SPEC:
* - start : id
* - return: id
@@ -2038,7 +2037,7 @@ end = struct (* {{{ *)
*)
let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp r_state_fb st ast);
- let Proof.{sigma} = Proof.data (Proof_global.give_me_the_proof ()) in
+ let Proof.{sigma} = Proof.data (Vernacstate.Proof_global.give_me_the_proof ()) in
match Evd.(evar_body (find sigma r_goal)) with
| Evd.Evar_empty -> RespNoProgress
| Evd.Evar_defined t ->
@@ -2066,7 +2065,7 @@ end = struct (* {{{ *)
module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) ()
let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id
- { indentation; verbose; loc; expr = e; strlen }
+ { indentation; verbose; loc; expr = e; strlen } : unit
=
let e, time, batch, fail =
let rec find ~time ~batch ~fail = function
@@ -2076,10 +2075,10 @@ end = struct (* {{{ *)
| e -> e, time, batch, fail in
find ~time:false ~batch:false ~fail:false e in
let st = Vernacstate.freeze_interp_state ~marshallable:false in
- Vernacentries.with_fail st fail (fun () ->
+ Vernacstate.Proof_global.with_fail ~st (fun () ->
(if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
ignore(TaskQueue.with_n_workers nworkers (fun queue ->
- Proof_global.with_current_proof (fun _ p ->
+ Vernacstate.Proof_global.with_current_proof (fun _ p ->
let Proof.{goals} = Proof.data p in
let open TacTask in
let res = CList.map_i (fun i g ->
@@ -2112,7 +2111,7 @@ end = struct (* {{{ *)
let open Notations in
match Future.join f with
| Some (pt, uc) ->
- let sigma, env = Pfedit.get_current_context () in
+ let sigma, env = Vernacstate.Proof_global.get_current_context () in
stm_pperr_endline (fun () -> hov 0 (
str"g=" ++ int (Evar.repr gid) ++ spc () ++
str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++
@@ -2392,10 +2391,10 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
(Proofview.Goal.goal gl) goals_to_admit then
Proofview.give_up else Proofview.tclUNIT ()
end in
- match VCS.get_state base_state with
+ match (VCS.get_info base_state).state with
| FullState { Vernacstate.proof } ->
- Proof_global.unfreeze proof;
- Proof_global.with_current_proof (fun _ p ->
+ Option.iter Vernacstate.Proof_global.unfreeze proof;
+ Vernacstate.Proof_global.with_current_proof (fun _ p ->
feedback ~id:id Feedback.AddedAxiom;
fst (Pfedit.solve Goal_select.SelectAll None tac p), ());
(* STATE SPEC:
@@ -2565,7 +2564,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
| VtKeepDefined -> Proof_global.Transparent
in
let proof =
- Proof_global.close_future_proof ~opaque ~feedback_id:id fp in
+ Vernacstate.Proof_global.close_future_proof ~opaque ~feedback_id:id fp in
if not delegate then ignore(Future.compute fp);
reach view.next;
let st = Vernacstate.freeze_interp_state ~marshallable:false in
@@ -2573,13 +2572,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
feedback ~id:id Incomplete
| { VCS.kind = `Master }, _ -> assert false
end;
- Proof_global.discard_all ()
+ Vernacstate.Proof_global.discard_all ()
), not redefine_qed, true
| `Sync (name, `Immediate) -> (fun () ->
reach eop;
let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp id st x);
- Proof_global.discard_all ()
+ Vernacstate.Proof_global.discard_all ()
), true, true
| `Sync (name, reason) -> (fun () ->
log_processing_sync id name reason;
@@ -2598,7 +2597,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
| VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent
| VtKeepAxiom -> assert false
in
- Some(Proof_global.close_proof ~opaque
+ Some(Vernacstate.Proof_global.close_proof ~opaque
~keep_body_ucst_separate:false
(State.exn_on id ~valid:eop)) in
if keep <> VtKeep VtKeepAxiom then
@@ -2609,7 +2608,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
let wall_clock3 = Unix.gettimeofday () in
Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time"
(Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
- Proof_global.discard_all ()
+ Vernacstate.Proof_global.discard_all ()
), true, true
| `MaybeASync (start, nodes, name, delegate) -> (fun () ->
reach ~cache:true start;
@@ -2870,7 +2869,7 @@ let merge_proof_branch ~valid ?id qast keep brname =
VCS.checkout VCS.Branch.master;
`Unfocus qed_id
| { VCS.kind = `Master } ->
- Exninfo.iraise (State.exn_on ~valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
+ Exninfo.iraise (State.exn_on ~valid Stateid.dummy (Vernacstate.Proof_global.NoCurrentProof, Exninfo.null))
(* When tty is true, this code also does some of the job of the user interface:
jump back to a state that is valid *)
@@ -3062,7 +3061,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
let st = Vernacstate.freeze_interp_state ~marshallable:false in
ignore(stm_vernac_interp id st x);
(* Vernac x may or may not start a proof *)
- if not in_proof && Proof_global.there_are_pending_proofs () then
+ if not in_proof && Vernacstate.Proof_global.there_are_pending_proofs () then
begin
let bname = VCS.mk_branch_name x in
let opacity_of_produced_term = function
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 3fe6ad0718..416ea88c1b 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -85,7 +85,7 @@ let ensure_exists f =
let compile opts copts ~echo ~f_in ~f_out =
let open Vernac.State in
let check_pending_proofs () =
- let pfs = Proof_global.get_all_proof_names () in
+ let pfs = Vernacstate.Proof_global.get_all_proof_names () in
if not (CList.is_empty pfs) then
fatal_error (str "There are pending proofs: "
++ (pfs
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index d4107177a7..fd4c515209 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -46,8 +46,9 @@ let coqc_main () =
outputstate copts;
flush_all();
+
if opts.Coqargs.output_context then begin
- let sigma, env = Pfedit.get_current_context () in
+ let sigma, env = let e = Global.env () in Evd.from_env e, e in
Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
end;
CProfile.print_profile ()
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 1094fc86b4..b3de8dd85f 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -191,8 +191,8 @@ end
from cycling. *)
let make_prompt () =
try
- (Names.Id.to_string (Proof_global.get_current_proof_name ())) ^ " < "
- with Proof_global.NoCurrentProof ->
+ (Names.Id.to_string (Vernacstate.Proof_global.get_current_proof_name ())) ^ " < "
+ with Vernacstate.Proof_global.NoCurrentProof ->
"Coq < "
(* the coq prompt added to the default one when in emacs mode
@@ -353,7 +353,7 @@ let print_anyway c =
let top_goal_print ~doc c oldp newp =
try
let proof_changed = not (Option.equal cproof oldp newp) in
- let print_goals = proof_changed && Proof_global.there_are_pending_proofs () ||
+ let print_goals = proof_changed && Vernacstate.Proof_global.there_are_pending_proofs () ||
print_anyway c in
if not !Flags.quiet && print_goals then begin
let dproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index ef1dc6993b..ce584f1109 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -70,7 +70,7 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) =
(* Force the command *)
let ndoc = if check then Stm.observe ~doc nsid else doc in
- let new_proof = Proof_global.give_me_the_proof_opt () in
+ let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () in
{ state with doc = ndoc; sid = nsid; proof = new_proof; }
with reraise ->
(* XXX: In non-interactive mode edit_at seems to do very weird
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 61b8cc3dcb..9d9318fb77 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -144,7 +144,7 @@ let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst
Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
instance_hook k pri global imps (ConstRef cst)
-let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype =
+let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype =
let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
if program_mode then
let hook _ _ vis gr =
@@ -163,33 +163,44 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
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 _progress = Obligations.add_definition id ?term:constr
+ ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls in
+ pstate
else
- Flags.silently (fun () ->
+ 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
- Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
+ 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));
+ (fun _ _ _ -> instance_hook k pri global imps ?hook)) in
(* spiwack: I don't know what to do with the status here. *)
- if not (Option.is_empty term) then
- let init_refine =
- Tacticals.New.tclTHENLIST [
- Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term)));
- Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
- Tactics.New.reduce_after_refine;
- ]
- in
- ignore (Pfedit.by init_refine)
- else ignore (Pfedit.by (Tactics.auto_intros_tac ids));
- (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ()
+ let pstate =
+ if not (Option.is_empty term) then
+ let init_refine =
+ Tacticals.New.tclTHENLIST [
+ Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (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 env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
+let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
let props =
match props with
| Some (true, { CAst.v = CRecord fs }) ->
@@ -269,12 +280,14 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct
Pretyping.check_evars env (Evd.from_env env) sigma termtype;
let termtype = to_constr sigma termtype in
let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
- if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
- declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype
- else if program_mode || refine || Option.is_empty props then
- declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
- else CErrors.user_err Pp.(str "Unsolved obligations remaining.");
- id
+ let pstate =
+ if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
+ (declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype;
+ None)
+ else if program_mode || refine || 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
+ else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in
+ id, pstate
let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl =
let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
@@ -318,7 +331,7 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl =
sigma, cl, u, c', ctx', ctx, imps, args, decl
-let new_instance ?(global=false) ?(refine= !refine_instance) ~program_mode
+let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mode
poly ctx (instid, bk, cl) props
?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
let env = Global.env() in
@@ -334,7 +347,7 @@ let new_instance ?(global=false) ?(refine= !refine_instance) ~program_mode
Namegen.next_global_ident_away i (Termops.vars_of_env env)
in
let env' = push_rel_context ctx env in
- do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
+ do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
cty k u ctx ctx' pri decl imps subst id props
let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) pri =
@@ -358,7 +371,7 @@ let named_of_rel_context l =
l ([], [])
in ctx
-let context poly l =
+let context ~pstate poly l =
let env = Global.env() in
let sigma = Evd.from_env env in
let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
@@ -431,7 +444,7 @@ let context poly l =
| Some b ->
let decl = (Discharge, poly, Definition) in
let entry = Declare.definition_entry ~univs ~types:t b in
- let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] in
+ let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in
Lib.sections_are_opened () || Lib.is_modtype_strict ()
in
status && nstatus
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 7e0ec42625..8954fde224 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -40,6 +40,7 @@ val declare_instance_constant :
unit
val new_instance :
+ pstate:Proof_global.t option ->
?global:bool (** Not global by default. *) ->
?refine:bool (** Allow refinement *) ->
program_mode:bool ->
@@ -51,7 +52,8 @@ val new_instance :
?tac:unit Proofview.tactic ->
?hook:(GlobRef.t -> unit) ->
Hints.hint_info_expr ->
- Id.t
+ (* May open a proof *)
+ Id.t * Proof_global.t option
val declare_new_instance :
?global:bool (** Not global by default. *) ->
@@ -74,4 +76,4 @@ val id_of_class : typeclass -> Id.t
(** returns [false] if, for lack of section, it declares an assumption
(unless in a module type). *)
-val context : Decl_kinds.polymorphic -> local_binder_expr list -> bool
+val context : pstate:Proof_global.t option -> Decl_kinds.polymorphic -> local_binder_expr list -> bool
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 37a33daf8f..27c5abf5ea 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -52,11 +52,12 @@ match local with
let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
let _ = declare_variable ident decl in
let () = assumption_message ident in
- let () =
- if not !Flags.quiet && Proof_global.there_are_pending_proofs () then
- Feedback.msg_info Pp.(str"Variable" ++ spc () ++ Id.print ident ++
- strbrk " is not visible from current goals")
- in
+ (* XXX *)
+ (* let () =
+ * if not !Flags.quiet && Proof_global.there_are_pending_proofs () then
+ * Feedback.msg_info (str"Variable" ++ spc () ++ Id.print ident ++
+ * strbrk " is not visible from current goals")
+ * in *)
let r = VarRef ident in
let () = maybe_declare_manual_implicits true r imps in
let () = Typeclasses.declare_instance None true r in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 28773a3965..feaf47df18 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -90,7 +90,7 @@ let check_definition ~program_mode (ce, evd, _, imps) =
check_evars_are_solved ~program_mode env evd;
ce
-let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
+let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
let (ce, evd, univdecl, imps as def) =
interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt
in
@@ -114,4 +114,4 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
let ce = check_definition ~program_mode def in
let uctx = Evd.evar_universe_context evd in
let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
- ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps )
+ ignore(DeclareDef.declare_definition ~ontop ident k ?hook_data ce (Evd.universe_binders evd) imps)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 9cb6190fcc..12853d83e0 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -16,11 +16,18 @@ open Constrexpr
(** {6 Definitions/Let} *)
-val do_definition : program_mode:bool ->
- ?hook:Lemmas.declaration_hook ->
- Id.t -> definition_kind -> universe_decl_expr option ->
- local_binder_expr list -> red_expr option -> constr_expr ->
- constr_expr option -> unit
+val do_definition
+ : ontop:Proof_global.t option
+ -> program_mode:bool
+ -> ?hook:Lemmas.declaration_hook
+ -> Id.t
+ -> definition_kind
+ -> universe_decl_expr option
+ -> local_binder_expr list
+ -> red_expr option
+ -> constr_expr
+ -> constr_expr option
+ -> unit
(************************************************************************)
(** Internal API *)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 2f00b41b7c..2aadbd224f 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -255,7 +255,8 @@ let interp_fixpoint ~cofix l ntns =
let uctx,fix = ground_fixpoint env evd fix in
(fix,pl,uctx,info)
-let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+let declare_fixpoint ~ontop 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 *)
let thms =
@@ -265,8 +266,9 @@ let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximp
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
fixdefs) in
let evd = Evd.from_ctx ctx in
- Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint)
- evd pl (Some(false,indexes,init_tac)) thms None
+ Some
+ (Lemmas.start_proof_with_initialization ~ontop (local,poly,DefinitionBody Fixpoint)
+ evd pl (Some(false,indexes,init_tac)) thms None)
else begin
(* We shortcut the proof process *)
let fixdefs = List.map Option.get fixdefs in
@@ -282,15 +284,18 @@ let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximp
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
- ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
+ ignore (List.map4 (DeclareDef.declare_fix ~ontop (local, poly, Fixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
fixpoint_message (Some indexes) fixnames;
- end;
+ None
+ end in
(* Declare notations *)
- List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
+ pstate
-let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+let declare_cofixpoint ~ontop 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 *)
let thms =
@@ -300,8 +305,8 @@ let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fixi
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
fixdefs) in
let evd = Evd.from_ctx ctx in
- Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
- evd pl (Some(true,[],init_tac)) thms None
+ Some (Lemmas.start_proof_with_initialization ~ontop (Global,poly, DefinitionBody CoFixpoint)
+ evd pl (Some(true,[],init_tac)) thms None)
else begin
(* We shortcut the proof process *)
let fixdefs = List.map Option.get fixdefs in
@@ -314,13 +319,15 @@ let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fixi
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
- ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
+ ignore (List.map4 (DeclareDef.declare_fix ~ontop (local, poly, CoFixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
- cofixpoint_message fixnames
- end;
+ cofixpoint_message fixnames;
+ None
+ end in
(* Declare notations *)
- List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
+ pstate
let extract_decreasing_argument limit = function
| (na,CStructRec) -> na
@@ -348,16 +355,18 @@ let check_safe () =
let flags = Environ.typing_flags (Global.env ()) in
flags.check_universes && flags.check_guarded
-let do_fixpoint local poly l =
+let do_fixpoint ~ontop local poly l =
let fixl, ntns = extract_fixpoint_components 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
- declare_fixpoint local poly fix possible_indexes ntns;
- if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+ let pstate = declare_fixpoint ~ontop local poly fix possible_indexes ntns in
+ if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
+ pstate
-let do_cofixpoint local poly l =
+let do_cofixpoint ~ontop local poly l =
let fixl,ntns = extract_cofixpoint_components l in
let cofix = interp_fixpoint ~cofix:true fixl ntns in
- declare_cofixpoint local poly cofix ntns;
- if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+ let pstate = declare_cofixpoint ~ontop 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 9bcb53697b..15ff5f4498 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -19,12 +19,14 @@ 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 -> unit
+ locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t option
val do_cofixpoint :
+ ontop:Proof_global.t option ->
(* When [false], assume guarded. *)
- locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
+ locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t option
(************************************************************************)
(** Internal API *)
@@ -81,15 +83,20 @@ 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 -> unit
+ Proof_global.lemma_possible_guards -> decl_notation list ->
+ Proof_global.t option
-val declare_cofixpoint : locality -> polymorphic ->
+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 -> unit
+ decl_notation list ->
+ Proof_global.t option
(** Very private function, do not use *)
val compute_possible_guardness_evidences :
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 7dcd098183..052832244b 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -33,12 +33,12 @@ let get_locality id ~kind = function
| Local -> true
| Global -> false
-let declare_definition ident (local, p, k) ?hook_data ce pl imps =
+let declare_definition ~ontop 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 () ->
let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in
- let () = if Proof_global.there_are_pending_proofs () then warn_definition_not_visible ident in
+ let () = if Option.has_some ontop then warn_definition_not_visible ident in
VarRef ident
| Discharge | Local | Global ->
let local = get_locality ident ~kind:"definition" local in
@@ -57,9 +57,9 @@ let declare_definition ident (local, p, k) ?hook_data ce pl imps =
end;
gr
-let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+let declare_fix ~ontop ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
- declare_definition f kind ?hook_data ce pl imps
+ declare_definition ~ontop f kind ?hook_data ce pl imps
let check_definition_evars ~allow_evars sigma =
let env = Global.env () in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 3f95ec7107..8e4f4bf7fb 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -14,7 +14,8 @@ open Decl_kinds
val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
val declare_definition
- : Id.t
+ : ontop:Proof_global.t option
+ -> Id.t
-> definition_kind
-> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
-> Safe_typing.private_constants Entries.definition_entry
@@ -23,7 +24,8 @@ val declare_definition
-> GlobRef.t
val declare_fix
- : ?opaque:bool
+ : ontop:Proof_global.t option
+ -> ?opaque:bool
-> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
-> definition_kind
-> UnivNames.universe_binders
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 0d0732cbb4..19b0856015 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -213,8 +213,11 @@ 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 () =
- let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in
+let fresh_name_for_anonymous_theorem ~pstate =
+ let avoid = match pstate with
+ | None -> Id.Set.empty
+ | Some pstate -> Id.Set.of_list (Proof_global.get_all_proof_names pstate)
+ in
next_global_ident_away default_thm_id avoid
let check_name_freshness locality {CAst.loc;v=id} : unit =
@@ -224,7 +227,7 @@ let check_name_freshness locality {CAst.loc;v=id} : unit =
then
user_err ?loc (Id.print id ++ str " already exists.")
-let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) =
+let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) =
let t_i = norm t_i in
let k = IsAssumption Conjectural in
match body with
@@ -260,7 +263,6 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,
| Lambda(na,ty,t) -> mkLambda(na,ty,body_i t)
| App (t, args) -> mkApp (body_i t, args)
| _ ->
- let sigma, env = Pfedit.get_current_context () in
anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in
let body_i = body_i body in
match locality with
@@ -333,7 +335,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 id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?(hook : declaration_hook option) c =
+let start_proof ~ontop 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
@@ -344,7 +346,7 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?(hook :
| 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
+ Proof_global.start_proof ~ontop sigma id ?pl kind goals terminator
let rec_tac_initializer finite guard thms snl =
if finite then
@@ -360,7 +362,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_proof_with_initialization ~ontop ?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) ->
@@ -386,18 +388,20 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in
let body = Option.map EConstr.of_constr body in
let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
- List.map_i (save_remaining_recthms kind norm uctx body opaq) 1 other_thms 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) ->
maybe_declare_manual_implicits false ref imps;
call_hook ?hook ctx [] strength ref) thms_data in
- start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard;
- ignore (Proof_global.with_current_proof (fun _ p ->
+ let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
+ let pstate, _ = Proof_global.with_current_proof (fun _ p ->
match init_tac with
| None -> p,(true,[])
- | Some tac -> Proof.run_tactic Global.(env ()) tac p))
+ | Some tac -> Proof.run_tactic Global.(env ()) tac p) pstate in
+ pstate
-let start_proof_com ~program_mode ?inference_hook ?hook kind thms =
+let start_proof_com ~program_mode ~ontop ?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
@@ -429,7 +433,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_proof_with_initialization ~ontop ?hook kind evd decl recguard thms snl
(* Saving a proof *)
@@ -444,7 +448,7 @@ let () =
optread = (fun () -> !keep_admitted_vars);
optwrite = (fun b -> keep_admitted_vars := b) }
-let save_proof ?proof = function
+let save_proof ?proof ~pstate = function
| Vernacexpr.Admitted ->
let pe =
let open Proof_global in
@@ -460,8 +464,8 @@ let save_proof ?proof = function
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 () in
- let gk = Proof_global.get_current_persistence () in
+ let pftree = Proof_global.give_me_the_proof pstate in
+ let gk = Proof_global.get_current_persistence pstate in
let Proof.{ name; poly; entry } = Proof.data pftree in
let typ = match Proofview.initial_goals entry with
| [typ] -> snd typ
@@ -473,10 +477,10 @@ let save_proof ?proof = function
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 () in
+ Proof_global.return_proof ~allow_partial:true pstate in
let sec_vars =
if not !keep_admitted_vars then None
- else match Proof_global.get_used_variables(), pproofs with
+ else match Proof_global.get_used_variables pstate, pproofs with
| Some _ as x, _ -> x
| None, (pproof, _) :: _ ->
let env = Global.env () in
@@ -484,18 +488,20 @@ let save_proof ?proof = function
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 () in
+ let decl = Proof_global.get_universe_decl pstate 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 ()) pe
+ Proof_global.apply_terminator (Proof_global.get_terminator pstate) pe;
+ Some pstate
| Vernacexpr.Proved (opaque,idopt) ->
let (proof_obj,terminator) =
match proof with
| None ->
- Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)
+ 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 *)
- if Option.is_empty proof then Proof_global.discard_current ();
- Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj)))
+ let pstate = if Option.is_empty proof then Proof_global.discard_current pstate else Some pstate in
+ Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj)));
+ pstate
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 72c666e903..9b5c84e0d1 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -37,30 +37,32 @@ val call_hook
-> ?fix_exn:Future.fix_exn
-> hook_type
-val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
+val start_proof : ontop:Proof_global.t option -> 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 -> unit
+ ?hook:declaration_hook -> EConstr.types -> Proof_global.t
-val start_proof_com :
- program_mode:bool -> ?inference_hook:Pretyping.inference_hook ->
- ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list ->
- unit
+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
-val start_proof_with_initialization :
+val start_proof_with_initialization : ontop:Proof_global.t option ->
?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 -> unit
+ (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
+ -> int list option -> Proof_global.t
val standard_proof_terminator :
?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
Proof_global.proof_terminator
-val fresh_name_for_anonymous_theorem : unit -> Id.t
+val fresh_name_for_anonymous_theorem : pstate:Proof_global.t option -> Id.t
(* Prepare global named context for proof session: remove proofs of
opaque section definitions and remove vm-compiled code *)
@@ -69,4 +71,4 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
(** {6 ... } *)
-val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
+val save_proof : ?proof:Proof_global.closed_proof -> pstate:Proof_global.t -> Vernacexpr.proof_end -> Proof_global.t option
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 9aca48f529..dc7d8ec1f0 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -456,7 +456,7 @@ let obligation_substitution expand prg =
let ints = intset_to (pred (Array.length obls)) in
obl_substitution expand obls ints
-let declare_definition prg =
+let declare_definition ~ontop prg =
let varsubst = obligation_substitution true prg in
let body, typ = subst_prog varsubst prg in
let nf = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None)
@@ -475,7 +475,7 @@ let declare_definition prg =
let () = progmap_remove prg in
let ubinders = UState.universe_binders uctx in
let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
- DeclareDef.declare_definition prg.prg_name
+ DeclareDef.declare_definition ~ontop prg.prg_name
prg.prg_kind ce ubinders prg.prg_implicits ?hook_data
let rec lam_index n t acc =
@@ -554,16 +554,14 @@ let declare_mutual_definition l =
(* Declare the recursive definitions *)
let univs = UState.univ_entry ~poly first.prg_ctx in
let fix_exn = Hook.get get_fix_exn () in
- let kns = List.map4
- (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
- fixnames fixdecls fixtypes fiximps
- in
- (* Declare notations *)
- List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
- Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
- let gr = List.hd kns in
- Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
- List.iter progmap_remove l; gr
+ let kns = List.map4 (DeclareDef.declare_fix ~ontop:None ~opaque (local, poly, kind) UnivNames.empty_binders univs)
+ fixnames fixdecls fixtypes fiximps in
+ (* Declare notations *)
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
+ Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
+ let gr = List.hd kns in
+ Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
+ List.iter progmap_remove l; gr
let decompose_lam_prod c ty =
let open Context.Rel.Declaration in
@@ -763,7 +761,7 @@ let update_obls prg obls rem =
else (
match prg'.prg_deps with
| [] ->
- let kn = declare_definition prg' in
+ let kn = declare_definition ~ontop:None prg' in
progmap_remove prg';
Defined kn
| l ->
@@ -948,7 +946,7 @@ let obligation_hook prg obl num auto ctx' _ _ gr =
ignore (auto (Some prg.prg_name) None deps)
end
-let rec solve_obligation prg num tac =
+let rec solve_obligation ?ontop prg num tac =
let user_num = succ num in
let obls, rem = prg.prg_obligations in
let obl = obls.(num) in
@@ -967,20 +965,21 @@ let rec solve_obligation prg num tac =
let auto n tac oblset = auto_solve_obligations n ~oblset tac in
let terminator ?hook guard =
Proof_global.make_terminator
- (obligation_terminator ?hook prg.prg_name num guard auto) in
+ (obligation_terminator prg.prg_name num guard ?hook auto) in
let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
- let () = Lemmas.start_proof ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
- let _ = Pfedit.by !default_tactic in
- Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac
+ 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 = 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 (user_num, name, typ) tac =
+and obligation ?ontop (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 prg num tac
+ | None -> solve_obligation ?ontop prg num tac
| Some r -> error "Obligation already solved"
else error (sprintf "Unknown obligation number %i" (succ num))
@@ -1113,7 +1112,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
let obls,_ = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
Flags.if_verbose Feedback.msg_info (info ++ str ".");
- let cst = declare_definition prg in
+ let cst = declare_definition ~ontop:None prg in
Defined cst)
else (
let len = Array.length obls in
@@ -1180,7 +1179,7 @@ let admit_obligations n =
let prg = get_prog_err n in
admit_prog prg
-let next_obligation n tac =
+let next_obligation ?ontop n tac =
let prg = match n with
| None -> get_any_prog_err ()
| Some _ -> get_prog_err n
@@ -1191,7 +1190,7 @@ let next_obligation n tac =
| Some i -> i
| None -> anomaly (Pp.str "Could not find a solvable obligation.")
in
- solve_obligation prg i tac
+ solve_obligation ?ontop 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 c5720363b4..eed3906a6a 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -85,10 +85,10 @@ val add_mutual_definitions :
notations ->
fixpoint_kind -> unit
-val obligation : int * Names.Id.t option * Constrexpr.constr_expr option ->
- Genarg.glob_generic_argument option -> unit
+val obligation : ?ontop:Proof_global.t -> int * Names.Id.t option * Constrexpr.constr_expr option ->
+ Genarg.glob_generic_argument option -> Proof_global.t
-val next_obligation : Names.Id.t option -> Genarg.glob_generic_argument option -> unit
+val next_obligation : ?ontop:Proof_global.t -> Names.Id.t option -> Genarg.glob_generic_argument option -> Proof_global.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/search.ml b/vernac/search.ml
index 6610789626..e41378908f 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -59,11 +59,16 @@ let iter_constructors indsp u fn env nconstr =
let iter_named_context_name_type f =
List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl))
+let get_current_or_goal_context ?pstate glnum =
+ match pstate with
+ | None -> let env = Global.env () in Evd.(from_env env, env)
+ | Some p -> Pfedit.get_goal_context p glnum
+
(* General search over hypothesis of a goal *)
-let iter_hypothesis glnum (fn : GlobRef.t -> env -> constr -> unit) =
+let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) =
let env = Global.env () in
let iter_hyp idh typ = fn (VarRef idh) env typ in
- let evmap,e = Pfedit.get_goal_context glnum in
+ let evmap,e = get_current_or_goal_context ?pstate glnum in
let pfctxt = named_context e in
iter_named_context_name_type iter_hyp pfctxt
@@ -99,10 +104,10 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
try Declaremods.iter_all_segments iter_obj
with Not_found -> ()
-let generic_search glnumopt fn =
+let generic_search ?pstate glnumopt fn =
(match glnumopt with
| None -> ()
- | Some glnum -> iter_hypothesis glnum fn);
+ | Some glnum -> iter_hypothesis ?pstate glnum fn);
iter_declarations fn
(** This module defines a preference on constrs in the form of a
@@ -221,7 +226,7 @@ let search_about_filter query gr env typ = match query with
(** SearchPattern *)
-let search_pattern gopt pat mods pr_search =
+let search_pattern ?pstate gopt pat mods pr_search =
let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
module_filter mods ref env typ &&
@@ -231,7 +236,7 @@ let search_pattern gopt pat mods pr_search =
let iter ref env typ =
if filter ref env typ then pr_search ref env typ
in
- generic_search gopt iter
+ generic_search ?pstate gopt iter
(** SearchRewrite *)
@@ -243,7 +248,7 @@ let rewrite_pat1 pat =
let rewrite_pat2 pat =
PApp (PRef (eq ()), [| PMeta None; PMeta None; pat |])
-let search_rewrite gopt pat mods pr_search =
+let search_rewrite ?pstate gopt pat mods pr_search =
let pat1 = rewrite_pat1 pat in
let pat2 = rewrite_pat2 pat in
let blacklist_filter = blacklist_filter_aux () in
@@ -256,11 +261,11 @@ let search_rewrite gopt pat mods pr_search =
let iter ref env typ =
if filter ref env typ then pr_search ref env typ
in
- generic_search gopt iter
+ generic_search ?pstate gopt iter
(** Search *)
-let search_by_head gopt pat mods pr_search =
+let search_by_head ?pstate gopt pat mods pr_search =
let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
module_filter mods ref env typ &&
@@ -270,11 +275,11 @@ let search_by_head gopt pat mods pr_search =
let iter ref env typ =
if filter ref env typ then pr_search ref env typ
in
- generic_search gopt iter
+ generic_search ?pstate gopt iter
(** SearchAbout *)
-let search_about gopt items mods pr_search =
+let search_about ?pstate gopt items mods pr_search =
let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
let eqb b1 b2 = if b1 then b2 else not b2 in
@@ -286,7 +291,7 @@ let search_about gopt items mods pr_search =
let iter ref env typ =
if filter ref env typ then pr_search ref env typ
in
- generic_search gopt iter
+ generic_search ?pstate gopt iter
type search_constraint =
| Name_Pattern of Str.regexp
@@ -301,7 +306,7 @@ type 'a coq_object = {
coq_object_object : 'a;
}
-let interface_search =
+let interface_search ?pstate =
let rec extract_flags name tpe subtpe mods blacklist = function
| [] -> (name, tpe, subtpe, mods, blacklist)
| (Name_Pattern regexp, b) :: l ->
@@ -371,7 +376,7 @@ let interface_search =
let iter ref env typ =
if filter_function ref env typ then print_function ref env typ
in
- let () = generic_search glnum iter in
+ let () = generic_search ?pstate glnum iter in
!ans
let blacklist_filter ref env typ =
diff --git a/vernac/search.mli b/vernac/search.mli
index ecbb02bc68..0f94ddc5b6 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 : int option -> constr_pattern -> DirPath.t list * bool
+val search_by_head : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
-> display_function -> unit
-val search_rewrite : int option -> constr_pattern -> DirPath.t list * bool
+val search_rewrite : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
-> display_function -> unit
-val search_pattern : int option -> constr_pattern -> DirPath.t list * bool
+val search_pattern : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
-> display_function -> unit
-val search_about : int option -> (bool * glob_search_about_item) list
+val search_about : ?pstate:Proof_global.t -> 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 : ?glnum:int -> (search_constraint * bool) list ->
+val interface_search : ?pstate:Proof_global.t -> ?glnum:int -> (search_constraint * bool) list ->
constr coq_object list
(** {6 Generic search function} *)
-val generic_search : int option -> display_function -> unit
+val generic_search : ?pstate:Proof_global.t -> 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 4250ddb02c..3ead8663ce 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -44,6 +44,28 @@ let vernac_pperr_endline pp =
(* Misc *)
+let there_are_pending_proofs ~pstate =
+ not Option.(is_empty pstate)
+
+let check_no_pending_proof ~pstate =
+ if there_are_pending_proofs ~pstate then
+ user_err Pp.(str "Command not supported (Open proofs remain)")
+
+let vernac_require_open_proof ~pstate f =
+ match pstate with
+ | Some pstate -> f ~pstate
+ | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)")
+
+let get_current_or_global_context ~pstate =
+ match pstate with
+ | None -> let env = Global.env () in Evd.(from_env env, env)
+ | Some p -> Pfedit.get_current_context p
+
+let get_goal_or_global_context ~pstate glnum =
+ match pstate with
+ | None -> let env = Global.env () in Evd.(from_env env, env)
+ | Some p -> Pfedit.get_goal_context p glnum
+
let cl_of_qualid = function
| FunClass -> Classops.CL_FUN
| SortClass -> Classops.CL_SORT
@@ -72,30 +94,36 @@ end
(*******************)
(* "Show" commands *)
-let show_proof () =
+let show_proof ~pstate =
(* spiwack: this would probably be cooler with a bit of polishing. *)
- let p = Proof_global.give_me_the_proof () in
- let sigma, env = Pfedit.get_current_context () in
- let pprf = Proof.partial_proof p in
- Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
+ try
+ let pstate = Option.get pstate in
+ let p = Proof_global.give_me_the_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
+ (* We print nothing if there are no goals left *)
+ with
+ | Pfedit.NoSuchGoal
+ | Option.IsNone -> mt ()
-let show_top_evars () =
+let show_top_evars ~pstate =
(* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
- let pfts = Proof_global.give_me_the_proof () in
+ let pfts = Proof_global.give_me_the_proof pstate in
let Proof.{goals;shelf;given_up;sigma} = Proof.data pfts in
pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma)
-let show_universes () =
- let pfts = Proof_global.give_me_the_proof () in
+let show_universes ~pstate =
+ let pfts = Proof_global.give_me_the_proof pstate in
let Proof.{goals;sigma} = Proof.data pfts 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 all =
+let show_intro ~pstate all =
let open EConstr in
- let pf = Proof_global.give_me_the_proof() in
+ let pf = Proof_global.give_me_the_proof pstate in
let Proof.{goals;sigma} = Proof.data pf in
if not (List.is_empty goals) then begin
let gl = {Evd.it=List.hd goals ; sigma = sigma; } in
@@ -224,7 +252,7 @@ let print_modtype qid =
with Not_found ->
user_err (str"Unknown Module Type or Module " ++ pr_qualid qid)
-let print_namespace ns =
+let print_namespace ~pstate ns =
let ns = List.rev (Names.DirPath.repr ns) in
(* [match_dirpath], [match_modulpath] are helpers for [matches]
which checks whether a constant is in the namespace [ns]. *)
@@ -272,10 +300,10 @@ let print_namespace ns =
let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in
print_list Id.print qn
in
- let print_constant k body =
+ let print_constant ~pstate k body =
(* FIXME: universes *)
let t = body.Declarations.const_type in
- let sigma, env = Pfedit.get_current_context () in
+ let sigma, env = get_current_or_global_context ~pstate in
print_kn k ++ str":" ++ spc() ++ Printer.pr_type_env env sigma t
in
let matches mp = match match_modulepath ns mp with
@@ -285,7 +313,7 @@ let print_namespace ns =
Environ.fold_constants (fun c body acc ->
let kn = Constant.user c in
if matches (KerName.modpath kn)
- then acc++fnl()++hov 2 (print_constant kn body)
+ then acc++fnl()++hov 2 (print_constant ~pstate kn body)
else acc)
(Global.env ()) (str"")
in
@@ -515,7 +543,7 @@ let () =
(***********)
(* Gallina *)
-let start_proof_and_print ~program_mode ?hook k l =
+let start_proof_and_print ~program_mode ~pstate ?hook k l =
let inference_hook =
if program_mode then
let hook env sigma ev =
@@ -537,7 +565,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_proof_com ~program_mode ~ontop:pstate ?inference_hook ?hook k l
let vernac_definition_hook p = function
| Coercion ->
@@ -548,7 +576,7 @@ let vernac_definition_hook p = function
Some (Class.add_subclass_hook p)
| _ -> None
-let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
+let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
let hook = vernac_definition_hook atts.polymorphic kind in
@@ -563,39 +591,42 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
let program_mode = atts.program in
let name =
match id with
- | Anonymous -> fresh_name_for_anonymous_theorem ()
+ | Anonymous -> fresh_name_for_anonymous_theorem ~pstate
| Name n -> n
in
(match def with
| ProveBody (bl,t) -> (* local binders, typ *)
- start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind)
- ?hook [(CAst.make ?loc name, pl), (bl, t)]
+ Some (start_proof_and_print ~program_mode ~pstate (local, atts.polymorphic, DefinitionBody kind)
+ ?hook [(CAst.make ?loc name, pl), (bl, t)])
| DefineBody (bl,red_option,c,typ_opt) ->
let red_option = match red_option with
- | None -> None
- | Some r ->
- let sigma, env = Pfedit.get_current_context () in
- 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)
-
-let vernac_start_proof ~atts kind l =
+ | None -> None
+ | Some r ->
+ let sigma, env = get_current_or_global_context ~pstate in
+ Some (snd (Hook.get f_interp_redexp env sigma r)) in
+ ComDefinition.do_definition ~ontop:pstate ~program_mode name
+ (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook;
+ pstate
+ )
+
+let vernac_start_proof ~atts ~pstate kind l =
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;
- start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l
+ Some (start_proof_and_print ~pstate ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l)
-let vernac_end_proof ?proof = function
- | Admitted -> save_proof ?proof Admitted
- | Proved (_,_) as e -> save_proof ?proof e
+let vernac_end_proof ~pstate ?proof = function
+ | Admitted -> save_proof ~pstate ?proof Admitted
+ | Proved (_,_) as e -> save_proof ~pstate ?proof e
-let vernac_exact_proof c =
+let vernac_exact_proof ~pstate c =
(* spiwack: for simplicity I do not enforce that "Proof proof_term" is
called only at the begining of a proof. *)
- let status = Pfedit.by (Tactics.exact_proof c) in
- save_proof (Vernacexpr.(Proved(Proof_global.Opaque,None)));
- if not status then Feedback.feedback Feedback.AddedAxiom
+ let pstate, status = Pfedit.by (Tactics.exact_proof c) pstate in
+ let pstate = save_proof ~pstate (Vernacexpr.(Proved(Proof_global.Opaque,None))) in
+ if not status then Feedback.feedback Feedback.AddedAxiom;
+ pstate
let vernac_assumption ~atts discharge kind l nl =
let open DefAttributes in
@@ -772,28 +803,28 @@ 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 discharge l =
+let vernac_fixpoint ~atts ~pstate discharge l : Proof_global.t option =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
if Dumpglob.dump () then
List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
(* XXX: Switch to the attribute system and match on ~atts *)
let do_fixpoint = if atts.program then
- ComProgramFixpoint.do_fixpoint
+ fun local sign l -> ComProgramFixpoint.do_fixpoint local sign l; None
else
- ComFixpoint.do_fixpoint
+ ComFixpoint.do_fixpoint ~ontop:pstate
in
do_fixpoint local atts.polymorphic l
-let vernac_cofixpoint ~atts discharge l =
+let vernac_cofixpoint ~atts ~pstate discharge l =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
if Dumpglob.dump () then
List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
let do_cofixpoint = if atts.program then
- ComProgramFixpoint.do_cofixpoint
+ fun local sign l -> ComProgramFixpoint.do_cofixpoint local sign l; None
else
- ComFixpoint.do_cofixpoint
+ ComFixpoint.do_cofixpoint ~ontop:pstate
in
do_cofixpoint local atts.polymorphic l
@@ -851,14 +882,14 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export
-let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
+let vernac_define_module ~pstate export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
if Lib.sections_are_opened () then
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
match mexpr_ast_l with
| [] ->
- Proof_global.check_no_pending_proof ();
+ check_no_pending_proof ~pstate;
let binders_ast,argsexport =
List.fold_right
(fun (export,idl,ty) (args,argsexport) ->
@@ -898,13 +929,13 @@ let vernac_end_module export {loc;v=id} =
Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined");
Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
-let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
+let vernac_declare_module_type ~pstate {loc;v=id} binders_ast mty_sign mty_ast_l =
if Lib.sections_are_opened () then
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
match mty_ast_l with
| [] ->
- Proof_global.check_no_pending_proof ();
+ check_no_pending_proof ~pstate;
let binders_ast,argsexport =
List.fold_right
(fun (export,idl,ty) (args,argsexport) ->
@@ -951,8 +982,8 @@ let vernac_include l =
(* Sections *)
-let vernac_begin_section ({v=id} as lid) =
- Proof_global.check_no_pending_proof ();
+let vernac_begin_section ~pstate ({v=id} as lid) =
+ check_no_pending_proof ~pstate;
Dumpglob.dump_definition lid true "sec";
Lib.open_section id
@@ -965,8 +996,8 @@ let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set
(* Dispatcher of the "End" command *)
-let vernac_end_segment ({v=id} as lid) =
- Proof_global.check_no_pending_proof ();
+let vernac_end_segment ~pstate ({v=id} as lid) =
+ check_no_pending_proof ~pstate;
match Lib.find_opening_node id with
| Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
| Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid
@@ -1031,7 +1062,7 @@ let vernac_instance ~atts sup inst props pri =
let global = not (make_section_locality atts.locality) in
Dumpglob.dump_constraint (fst (pi1 inst)) false "inst";
let program_mode = atts.program in
- ignore(Classes.new_instance ~program_mode ~global atts.polymorphic sup inst props pri)
+ Classes.new_instance ~program_mode ~global atts.polymorphic sup inst props pri
let vernac_declare_instance ~atts sup inst pri =
let open DefAttributes in
@@ -1039,8 +1070,8 @@ let vernac_declare_instance ~atts sup inst pri =
Dumpglob.dump_definition (fst (pi1 inst)) false "inst";
Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri
-let vernac_context ~poly l =
- if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
+let vernac_context ~pstate ~poly l =
+ if not (Classes.context ~pstate poly l) then Feedback.feedback Feedback.AddedAxiom
let vernac_existing_instance ~section_local insts =
let glob = not section_local in
@@ -1061,21 +1092,19 @@ let focus_command_cond = Proof.no_cond command_focus
there are no more goals to solve. It cannot be a tactic since
all tactics fail if there are no further goals to prove. *)
-let vernac_solve_existential = Pfedit.instantiate_nth_evar_com
+let vernac_solve_existential ~pstate i e = Pfedit.instantiate_nth_evar_com i e pstate
-let vernac_set_end_tac tac =
+let vernac_set_end_tac ~pstate tac =
let env = Genintern.empty_glob_sign (Global.env ()) in
let _, tac = Genintern.generic_intern env tac in
- if not (Proof_global.there_are_pending_proofs ()) then
- user_err Pp.(str "Unknown command of the non proof-editing mode.");
- Proof_global.set_endline_tactic tac
- (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
+ (* 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 e =
+let vernac_set_used_variables ~(pstate : Proof_global.t) 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 ())) in
+ List.map snd (initial_goals (Proof_global.give_me_the_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
@@ -1084,10 +1113,10 @@ let vernac_set_used_variables e =
user_err ~hdr:"vernac_set_used_variables"
(str "Unknown variable: " ++ Id.print id))
l;
- ignore (Proof_global.set_used_variables l);
- Proof_global.with_current_proof begin fun _ p ->
+ let _, pstate = Proof_global.set_used_variables pstate l in
+ fst @@ Proof_global.with_current_proof begin fun _ p ->
(p, ())
- end
+ end pstate
(*****************************)
(* Auxiliary file management *)
@@ -1132,12 +1161,10 @@ let vernac_chdir = function
(* State management *)
let vernac_write_state file =
- Proof_global.discard_all ();
let file = CUnix.make_suffix file ".coq" in
States.extern_state file
let vernac_restore_state file =
- Proof_global.discard_all ();
let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in
States.intern_state file
@@ -1730,9 +1757,14 @@ let vernac_print_option key =
try print_option_value key
with Not_found -> error_undeclared_key key
-let get_current_context_of_args = function
- | Some n -> Pfedit.get_goal_context n
- | None -> Pfedit.get_current_context ()
+let get_current_context_of_args ~pstate =
+ match pstate with
+ | None -> fun _ ->
+ let env = Global.env () in Evd.(from_env env, env)
+ | Some pstate ->
+ function
+ | Some n -> Pfedit.get_goal_context pstate n
+ | None -> Pfedit.get_current_context pstate
let query_command_selector ?loc = function
| None -> None
@@ -1740,9 +1772,9 @@ let query_command_selector ?loc = function
| _ -> user_err ?loc ~hdr:"query_command_selector"
(str "Query commands only support the single numbered goal selector.")
-let vernac_check_may_eval ~atts redexp glopt rc =
+let vernac_check_may_eval ~pstate ~atts redexp glopt rc =
let glopt = query_command_selector glopt in
- let (sigma, env) = get_current_context_of_args glopt in
+ let sigma, env = get_current_context_of_args ~pstate glopt in
let sigma, c = interp_open_constr env sigma rc in
let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
Evarconv.check_problems_are_solved env sigma;
@@ -1796,27 +1828,33 @@ let vernac_global_check c =
pr_universe_ctx_set sigma uctx
-let get_nth_goal n =
- let pf = Proof_global.give_me_the_proof() in
+let get_nth_goal ~pstate n =
+ let pf = Proof_global.give_me_the_proof pstate in
let Proof.{goals;sigma} = Proof.data pf in
let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in
gl
exception NoHyp
+
(* Printing "About" information of a hypothesis of the current goal.
We only print the type and a small statement to this comes from the
goal. Precondition: there must be at least one current goal. *)
-let print_about_hyp_globs ?loc ref_or_by_not udecl glopt =
+let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
let open Context.Named.Declaration in
try
+ (* Fallback early to globals *)
+ let pstate = match pstate with
+ | None -> raise Not_found
+ | Some pstate -> pstate
+ in
(* FIXME error on non None udecl if we find the hyp. *)
let glnumopt = query_command_selector ?loc glopt in
let gl,id =
match glnumopt, ref_or_by_not.v with
| None,AN qid when qualid_is_ident qid -> (* goal number not given, catch any failure *)
- (try get_nth_goal 1, qualid_basename qid with _ -> raise NoHyp)
+ (try get_nth_goal ~pstate 1, qualid_basename qid with _ -> raise NoHyp)
| Some n,AN qid when qualid_is_ident qid -> (* goal number given, catch if wong *)
- (try get_nth_goal n, qualid_basename qid
+ (try get_nth_goal ~pstate n, qualid_basename qid
with
Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs"
(str "No such goal: " ++ int n ++ str "."))
@@ -1826,15 +1864,16 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt =
let natureofid = match decl with
| LocalAssum _ -> "Hypothesis"
| LocalDef (_,bdy,_) ->"Constant (let in)" in
- let sigma, env = Pfedit.get_current_context () in
+ let sigma, env = Pfedit.get_current_context pstate in
v 0 (Id.print id ++ str":" ++ pr_econstr_env env sigma (NamedDecl.get_type decl) ++ fnl() ++ fnl()
++ str natureofid ++ str " of the goal context.")
with (* fallback to globals *)
| NoHyp | Not_found ->
- let sigma, env = Pfedit.get_current_context () in
+ let sigma, env = get_current_or_global_context ~pstate in
print_about env sigma ref_or_by_not udecl
-let vernac_print ~atts env sigma =
+let vernac_print ~(pstate : Proof_global.t option) ~atts =
+ let sigma, env = get_current_or_global_context ~pstate in
function
| PrintTables -> print_tables ()
| PrintFullContext-> print_full_context_typ env sigma
@@ -1845,7 +1884,7 @@ let vernac_print ~atts env sigma =
| PrintModules -> print_modules ()
| PrintModule qid -> print_module qid
| PrintModuleType qid -> print_modtype qid
- | PrintNamespace ns -> print_namespace ns
+ | PrintNamespace ns -> print_namespace ~pstate ns
| PrintMLLoadPath -> Mltop.print_ml_path ()
| PrintMLModules -> Mltop.print_ml_modules ()
| PrintDebugGC -> Mltop.print_gc ()
@@ -1862,7 +1901,13 @@ let vernac_print ~atts env sigma =
| PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma
| PrintUniverses (sort, subgraph, dst) -> print_universes ~sort ~subgraph dst
| PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r)
- | PrintHintGoal -> Hints.pr_applicable_hint ()
+ | PrintHintGoal ->
+ begin match pstate with
+ | Some pstate ->
+ Hints.pr_applicable_hint pstate
+ | None ->
+ str "No proof in progress"
+ end
| PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s
| PrintHintDb -> Hints.pr_searchtable env sigma
| PrintScopes ->
@@ -1872,7 +1917,7 @@ let vernac_print ~atts env sigma =
| PrintVisibility s ->
Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s
| PrintAbout (ref_or_by_not,udecl,glnumopt) ->
- print_about_hyp_globs ref_or_by_not udecl glnumopt
+ print_about_hyp_globs ~pstate ref_or_by_not udecl glnumopt
| PrintImplicit qid ->
dump_global qid;
print_impargs qid
@@ -1937,16 +1982,16 @@ let () =
optread = (fun () -> !search_output_name_only);
optwrite = (:=) search_output_name_only }
-let vernac_search ~atts s gopt r =
+let vernac_search ~pstate ~atts s gopt r =
let gopt = query_command_selector gopt in
let r = interp_search_restriction r in
let env,gopt =
match gopt with | None ->
(* 1st goal by default if it exists, otherwise no goal at all *)
- (try snd (Pfedit.get_goal_context 1) , Some 1
+ (try snd (get_goal_or_global_context ~pstate 1) , Some 1
with _ -> Global.env (),None)
(* if goal selector is given and wrong, then let exceptions be raised. *)
- | Some g -> snd (Pfedit.get_goal_context g) , Some g
+ | Some g -> snd (get_goal_or_global_context ~pstate g) , Some g
in
let get_pattern c = snd (intern_constr_pattern env Evd.(from_env env) c) in
let pr_search ref env c =
@@ -1961,21 +2006,21 @@ let vernac_search ~atts s gopt r =
in
match s with
| SearchPattern c ->
- (Search.search_pattern gopt (get_pattern c) r |> Search.prioritize_search) pr_search
+ (Search.search_pattern ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
| SearchRewrite c ->
- (Search.search_rewrite gopt (get_pattern c) r |> Search.prioritize_search) pr_search
+ (Search.search_rewrite ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
| SearchHead c ->
- (Search.search_by_head gopt (get_pattern c) r |> Search.prioritize_search) pr_search
+ (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
| SearchAbout sl ->
- (Search.search_about gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |>
+ (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |>
Search.prioritize_search) pr_search
-let vernac_locate = function
+let vernac_locate ~pstate = function
| LocateAny {v=AN qid} -> print_located_qualid qid
| LocateTerm {v=AN qid} -> print_located_term qid
| LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *)
| LocateTerm {v=ByNotation (ntn, sc)} ->
- let _, env = Pfedit.get_current_context () in
+ let _, env = get_current_or_global_context ~pstate in
Notation.locate_notation
(Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc
| LocateLibrary qid -> print_located_library qid
@@ -1983,9 +2028,9 @@ let vernac_locate = function
| LocateOther (s, qid) -> print_located_other s qid
| LocateFile f -> locate_file f
-let vernac_register qid r =
+let vernac_register ~pstate qid r =
let gr = Smartlocate.global_with_alias qid in
- if Proof_global.there_are_pending_proofs () then
+ if there_are_pending_proofs ~pstate then
user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
match r with
| RegisterInline ->
@@ -2029,8 +2074,8 @@ let vernac_unfocus () =
(fun _ p -> Proof.unfocus command_focus p ())
(* Checks that a proof is fully unfocused. Raises an error if not. *)
-let vernac_unfocused () =
- let p = Proof_global.give_me_the_proof () in
+let vernac_unfocused ~pstate =
+ let p = Proof_global.give_me_the_proof pstate in
if Proof.unfocused p then
str"The proof is indeed fully unfocused."
else
@@ -2060,25 +2105,38 @@ let vernac_bullet (bullet : Proof_bullet.t) =
Proof_global.simple_with_current_proof (fun _ p ->
Proof_bullet.put p bullet)
-let vernac_show = function
- | ShowScript -> assert false (* Only the stm knows the script *)
- | ShowGoal goalref ->
- let proof = Proof_global.give_me_the_proof () 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
+let vernac_show ~pstate =
+ match pstate with
+ (* Show functions that don't require a proof state *)
+ | None ->
+ begin function
+ | ShowProof -> show_proof ~pstate
+ | ShowMatch id -> show_match id
+ | ShowScript -> assert false (* Only the stm knows the script *)
+ | _ -> mt ()
+ end
+ (* Show functions that require a proof state *)
+ | Some pstate ->
+ 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
+ | ShowProofNames ->
+ pr_sequence Id.print (Proof_global.get_all_proof_names pstate)
+ | ShowIntros all -> show_intro ~pstate all
+ | ShowProof -> show_proof ~pstate:(Some pstate)
+ | ShowMatch id -> show_match id
+ | ShowScript -> assert false (* Only the stm knows the script *)
end
- | ShowProof -> show_proof ()
- | ShowExistentials -> show_top_evars ()
- | ShowUniverses -> show_universes ()
- | ShowProofNames ->
- pr_sequence Id.print (Proof_global.get_all_proof_names())
- | ShowIntros all -> show_intro all
- | ShowMatch id -> show_match id
-
-let vernac_check_guard () =
- let pts = Proof_global.give_me_the_proof () in
+
+let vernac_check_guard ~pstate =
+ let pts = Proof_global.give_me_the_proof pstate in
let pfterm = List.hd (Proof.partial_proof pts) in
let message =
try
@@ -2097,8 +2155,9 @@ exception End_of_input
the way the proof mode is set there makes the task non trivial
without a considerable amount of refactoring.
*)
-let vernac_load interp fname =
- if Proof_global.there_are_pending_proofs () then
+let vernac_load ~st interp fname =
+ let pstate = st.Vernacstate.proof in
+ if there_are_pending_proofs ~pstate then
CErrors.user_err Pp.(str "Load is not supported inside proofs.");
let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
(fun po ->
@@ -2112,21 +2171,21 @@ let vernac_load interp fname =
let longfname = Loadpath.locate_file fname in
let in_chan = open_utf8_file_in longfname in
Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
- begin
- try while true do
- let proof_mode =
- if Proof_global.there_are_pending_proofs () then
- Some (get_default_proof_mode ())
- else
- None
- in
- interp (parse_sentence proof_mode input).CAst.v;
- done
- with End_of_input -> ()
- end;
+ let rec load_loop ~pstate =
+ try
+ let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) pstate in
+ let pstate = interp ~st:{ st with Vernacstate.proof = pstate }
+ (parse_sentence proof_mode input).CAst.v in
+ load_loop ~pstate
+ with
+ End_of_input ->
+ pstate
+ in
+ let pstate = load_loop ~pstate in
(* If Load left a proof open, we fail too. *)
- if Proof_global.there_are_pending_proofs () then
- CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.")
+ if there_are_pending_proofs ~pstate then
+ CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
+ pstate
let with_locality ~atts f =
let local = Attributes.(parse locality atts) in
@@ -2151,7 +2210,8 @@ let with_def_attributes ~atts f =
* is the outdated/deprecated "Local" attribute of some vernacular commands
* still parsed as the obsolete_locality grammar entry for retrocompatibility.
* loc is the Loc.t of the vernacular command being interpreted. *)
-let interp ?proof ~atts ~st c =
+let interp ?proof ~atts ~st c : Proof_global.t option =
+ let pstate = st.Vernacstate.proof in
vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
match c with
@@ -2175,145 +2235,309 @@ let interp ?proof ~atts ~st c =
(* Syntax *)
| VernacSyntaxExtension (infix, sl) ->
- with_module_locality ~atts vernac_syntax_extension infix sl
- | VernacDeclareScope sc -> with_module_locality ~atts vernac_declare_scope sc
- | VernacDelimiters (sc,lr) -> with_module_locality ~atts vernac_delimiters sc lr
- | VernacBindScope (sc,rl) -> with_module_locality ~atts vernac_bind_scope sc rl
- | VernacOpenCloseScope (b, s) -> with_section_locality ~atts vernac_open_close_scope (b,s)
- | VernacInfix (mv,qid,sc) -> with_module_locality ~atts vernac_infix mv qid sc
- | VernacNotation (c,infpl,sc) -> with_module_locality ~atts vernac_notation c infpl sc
+ with_module_locality ~atts vernac_syntax_extension infix sl;
+ pstate
+ | VernacDeclareScope sc ->
+ with_module_locality ~atts vernac_declare_scope sc;
+ pstate
+ | VernacDelimiters (sc,lr) ->
+ with_module_locality ~atts vernac_delimiters sc lr;
+ pstate
+ | VernacBindScope (sc,rl) ->
+ with_module_locality ~atts vernac_bind_scope sc rl;
+ pstate
+ | VernacOpenCloseScope (b, s) ->
+ with_section_locality ~atts vernac_open_close_scope (b,s);
+ pstate
+ | VernacInfix (mv,qid,sc) ->
+ with_module_locality ~atts vernac_infix mv qid sc;
+ pstate
+ | VernacNotation (c,infpl,sc) ->
+ with_module_locality ~atts vernac_notation c infpl sc;
+ pstate
| VernacNotationAddFormat(n,k,v) ->
unsupported_attributes atts;
- Metasyntax.add_notation_extra_printing_rule n k v
+ Metasyntax.add_notation_extra_printing_rule n k v;
+ pstate
| VernacDeclareCustomEntry s ->
- with_module_locality ~atts vernac_custom_entry s
+ with_module_locality ~atts vernac_custom_entry s;
+ pstate
(* Gallina *)
| VernacDefinition ((discharge,kind),lid,d) ->
- with_def_attributes ~atts vernac_definition discharge kind lid d
- | VernacStartTheoremProof (k,l) -> with_def_attributes vernac_start_proof ~atts k l
- | VernacEndProof e -> unsupported_attributes atts; vernac_end_proof ?proof e
- | VernacExactProof c -> unsupported_attributes atts; vernac_exact_proof c
+ with_def_attributes ~atts vernac_definition ~pstate discharge kind lid d
+ | VernacStartTheoremProof (k,l) ->
+ with_def_attributes ~atts vernac_start_proof ~pstate k l
+ | VernacEndProof e ->
+ unsupported_attributes atts;
+ vernac_require_open_proof ~pstate (vernac_end_proof ?proof e)
+ | VernacExactProof c ->
+ unsupported_attributes atts;
+ vernac_require_open_proof ~pstate (vernac_exact_proof c)
| VernacAssumption ((discharge,kind),nl,l) ->
- with_def_attributes vernac_assumption ~atts discharge kind l nl
- | VernacInductive (cum, priv, finite, l) -> vernac_inductive ~atts cum priv finite l
- | VernacFixpoint (discharge, l) -> with_def_attributes vernac_fixpoint ~atts discharge l
- | VernacCoFixpoint (discharge, l) -> with_def_attributes vernac_cofixpoint ~atts discharge l
- | VernacScheme l -> unsupported_attributes atts; vernac_scheme l
- | VernacCombinedScheme (id, l) -> unsupported_attributes atts; vernac_combined_scheme id l
- | VernacUniverse l -> vernac_universe ~poly:(only_polymorphism atts) l
- | VernacConstraint l -> vernac_constraint ~poly:(only_polymorphism atts) l
+ with_def_attributes ~atts vernac_assumption discharge kind l nl;
+ pstate
+ | VernacInductive (cum, priv, finite, l) ->
+ vernac_inductive ~atts cum priv finite l;
+ pstate
+ | VernacFixpoint (discharge, l) ->
+ with_def_attributes ~atts vernac_fixpoint ~pstate discharge l
+ | VernacCoFixpoint (discharge, l) ->
+ with_def_attributes ~atts vernac_cofixpoint ~pstate discharge l
+ | VernacScheme l ->
+ unsupported_attributes atts;
+ vernac_scheme l;
+ pstate
+ | VernacCombinedScheme (id, l) ->
+ unsupported_attributes atts;
+ vernac_combined_scheme id l;
+ pstate
+ | VernacUniverse l ->
+ vernac_universe ~poly:(only_polymorphism atts) l;
+ pstate
+ | VernacConstraint l ->
+ vernac_constraint ~poly:(only_polymorphism atts) l;
+ pstate
(* Modules *)
| VernacDeclareModule (export,lid,bl,mtyo) ->
- unsupported_attributes atts; vernac_declare_module export lid bl mtyo
+ unsupported_attributes atts;
+ vernac_declare_module export lid bl mtyo;
+ pstate
| VernacDefineModule (export,lid,bl,mtys,mexprl) ->
- unsupported_attributes atts; vernac_define_module export lid bl mtys mexprl
+ unsupported_attributes atts;
+ vernac_define_module ~pstate export lid bl mtys mexprl;
+ pstate
| VernacDeclareModuleType (lid,bl,mtys,mtyo) ->
- unsupported_attributes atts; vernac_declare_module_type lid bl mtys mtyo
+ unsupported_attributes atts;
+ vernac_declare_module_type ~pstate lid bl mtys mtyo;
+ pstate
| VernacInclude in_asts ->
- unsupported_attributes atts; vernac_include in_asts
+ unsupported_attributes atts;
+ vernac_include in_asts;
+ pstate
(* Gallina extensions *)
- | VernacBeginSection lid -> unsupported_attributes atts; vernac_begin_section lid
+ | VernacBeginSection lid ->
+ unsupported_attributes atts;
+ vernac_begin_section ~pstate lid;
+ pstate
- | VernacEndSegment lid -> unsupported_attributes atts; vernac_end_segment lid
+ | VernacEndSegment lid ->
+ unsupported_attributes atts;
+ vernac_end_segment ~pstate lid;
+ pstate
- | VernacNameSectionHypSet (lid, set) -> unsupported_attributes atts; vernac_name_sec_hyp lid set
+ | VernacNameSectionHypSet (lid, set) ->
+ unsupported_attributes atts;
+ vernac_name_sec_hyp lid set;
+ pstate
- | VernacRequire (from, export, qidl) -> unsupported_attributes atts; vernac_require from export qidl
- | VernacImport (export,qidl) -> unsupported_attributes atts; vernac_import export qidl
- | VernacCanonical qid -> unsupported_attributes atts; vernac_canonical qid
- | VernacCoercion (r,s,t) -> vernac_coercion ~atts r s t
+ | VernacRequire (from, export, qidl) ->
+ unsupported_attributes atts;
+ vernac_require from export qidl;
+ pstate
+ | VernacImport (export,qidl) ->
+ unsupported_attributes atts;
+ vernac_import export qidl;
+ pstate
+ | VernacCanonical qid ->
+ unsupported_attributes atts;
+ vernac_canonical qid;
+ pstate
+ | VernacCoercion (r,s,t) ->
+ vernac_coercion ~atts r s t;
+ pstate
| VernacIdentityCoercion ({v=id},s,t) ->
- vernac_identity_coercion ~atts id s t
+ vernac_identity_coercion ~atts id s t;
+ pstate
(* Type classes *)
| VernacInstance (sup, inst, props, info) ->
- with_def_attributes vernac_instance ~atts sup inst props info
+ snd @@ with_def_attributes ~atts (vernac_instance ~pstate sup inst props info)
| VernacDeclareInstance (sup, inst, info) ->
- with_def_attributes vernac_declare_instance ~atts sup inst info
- | VernacContext sup -> vernac_context ~poly:(only_polymorphism atts) sup
- | VernacExistingInstance insts -> with_section_locality ~atts vernac_existing_instance insts
- | VernacExistingClass id -> unsupported_attributes atts; vernac_existing_class id
+ with_def_attributes ~atts vernac_declare_instance sup inst info;
+ pstate
+ | VernacContext sup ->
+ let () = vernac_context ~pstate ~poly:(only_polymorphism atts) sup in
+ pstate
+ | VernacExistingInstance insts ->
+ with_section_locality ~atts vernac_existing_instance insts;
+ pstate
+ | VernacExistingClass id ->
+ unsupported_attributes atts;
+ vernac_existing_class id;
+ pstate
(* Solving *)
- | VernacSolveExistential (n,c) -> unsupported_attributes atts; vernac_solve_existential n c
+ | VernacSolveExistential (n,c) ->
+ unsupported_attributes atts;
+ Some (vernac_require_open_proof ~pstate (vernac_solve_existential n c))
(* Auxiliary file and library management *)
- | VernacAddLoadPath (isrec,s,alias) -> unsupported_attributes atts; vernac_add_loadpath isrec s alias
- | VernacRemoveLoadPath s -> unsupported_attributes atts; vernac_remove_loadpath s
- | VernacAddMLPath (isrec,s) -> unsupported_attributes atts; vernac_add_ml_path isrec s
- | VernacDeclareMLModule l -> with_locality ~atts vernac_declare_ml_module l
- | VernacChdir s -> unsupported_attributes atts; vernac_chdir s
+ | VernacAddLoadPath (isrec,s,alias) ->
+ unsupported_attributes atts;
+ vernac_add_loadpath isrec s alias;
+ pstate
+ | VernacRemoveLoadPath s ->
+ unsupported_attributes atts;
+ vernac_remove_loadpath s;
+ pstate
+ | VernacAddMLPath (isrec,s) ->
+ unsupported_attributes atts;
+ vernac_add_ml_path isrec s;
+ pstate
+ | VernacDeclareMLModule l ->
+ with_locality ~atts vernac_declare_ml_module l;
+ pstate
+ | VernacChdir s ->
+ unsupported_attributes atts;
+ vernac_chdir s;
+ pstate
(* State management *)
- | VernacWriteState s -> unsupported_attributes atts; vernac_write_state s
- | VernacRestoreState s -> unsupported_attributes atts; vernac_restore_state s
+ | VernacWriteState s ->
+ unsupported_attributes atts;
+ vernac_write_state s;
+ pstate
+ | VernacRestoreState s ->
+ unsupported_attributes atts;
+ vernac_restore_state s;
+ pstate
(* Commands *)
| VernacCreateHintDb (dbname,b) ->
- with_module_locality ~atts vernac_create_hintdb dbname b
+ with_module_locality ~atts vernac_create_hintdb dbname b;
+ pstate
| VernacRemoveHints (dbnames,ids) ->
- with_module_locality ~atts vernac_remove_hints dbnames ids
+ with_module_locality ~atts vernac_remove_hints dbnames ids;
+ pstate
| VernacHints (dbnames,hints) ->
- vernac_hints ~atts dbnames hints
+ vernac_hints ~atts dbnames hints;
+ pstate
| VernacSyntacticDefinition (id,c,b) ->
- with_module_locality ~atts vernac_syntactic_definition id c b
+ with_module_locality ~atts vernac_syntactic_definition id c b;
+ pstate
| VernacArguments (qid, args, more_implicits, nargs, flags) ->
- with_section_locality ~atts vernac_arguments qid args more_implicits nargs flags
- | VernacReserve bl -> unsupported_attributes atts; vernac_reserve bl
- | VernacGeneralizable gen -> with_locality ~atts vernac_generalizable gen
- | VernacSetOpacity qidl -> with_locality ~atts vernac_set_opacity qidl
- | VernacSetStrategy l -> with_locality ~atts vernac_set_strategy l
- | VernacSetOption (export, key,v) -> vernac_set_option ~local:(only_locality atts) export key v
- | VernacUnsetOption (export, key) -> vernac_unset_option ~local:(only_locality atts) export key
- | VernacRemoveOption (key,v) -> unsupported_attributes atts; vernac_remove_option key v
- | VernacAddOption (key,v) -> unsupported_attributes atts; vernac_add_option key v
- | VernacMemOption (key,v) -> unsupported_attributes atts; vernac_mem_option key v
- | VernacPrintOption key -> unsupported_attributes atts; vernac_print_option key
+ with_section_locality ~atts vernac_arguments qid args more_implicits nargs flags;
+ pstate
+ | VernacReserve bl ->
+ unsupported_attributes atts;
+ vernac_reserve bl;
+ pstate
+ | VernacGeneralizable gen ->
+ with_locality ~atts vernac_generalizable gen;
+ pstate
+ | VernacSetOpacity qidl ->
+ with_locality ~atts vernac_set_opacity qidl;
+ pstate
+ | VernacSetStrategy l ->
+ with_locality ~atts vernac_set_strategy l;
+ pstate
+ | VernacSetOption (export, key,v) ->
+ vernac_set_option ~local:(only_locality atts) export key v;
+ pstate
+ | VernacUnsetOption (export, key) ->
+ vernac_unset_option ~local:(only_locality atts) export key;
+ pstate
+ | VernacRemoveOption (key,v) ->
+ unsupported_attributes atts;
+ vernac_remove_option key v;
+ pstate
+ | VernacAddOption (key,v) ->
+ unsupported_attributes atts;
+ vernac_add_option key v;
+ pstate
+ | VernacMemOption (key,v) ->
+ unsupported_attributes atts;
+ vernac_mem_option key v;
+ pstate
+ | VernacPrintOption key ->
+ unsupported_attributes atts;
+ vernac_print_option key;
+ pstate
| VernacCheckMayEval (r,g,c) ->
- Feedback.msg_notice @@ vernac_check_may_eval ~atts r g c
- | VernacDeclareReduction (s,r) -> with_locality ~atts vernac_declare_reduction s r
+ Feedback.msg_notice @@
+ vernac_check_may_eval ~pstate ~atts r g c;
+ pstate
+ | VernacDeclareReduction (s,r) ->
+ with_locality ~atts vernac_declare_reduction s r;
+ pstate
| VernacGlobalCheck c ->
unsupported_attributes atts;
- Feedback.msg_notice @@ vernac_global_check c
+ Feedback.msg_notice @@ vernac_global_check c;
+ pstate
| VernacPrint p ->
- let sigma, env = Pfedit.get_current_context () in
- Feedback.msg_notice @@ vernac_print ~atts env sigma p
- | VernacSearch (s,g,r) -> unsupported_attributes atts; vernac_search ~atts s g r
+ Feedback.msg_notice @@ vernac_print ~pstate ~atts p;
+ pstate
+ | VernacSearch (s,g,r) ->
+ unsupported_attributes atts;
+ vernac_search ~pstate ~atts s g r;
+ pstate
| VernacLocate l -> unsupported_attributes atts;
- Feedback.msg_notice @@ vernac_locate l
- | VernacRegister (qid, r) -> unsupported_attributes atts; vernac_register qid r
- | VernacPrimitive (id, prim, typopt) -> unsupported_attributes atts; ComAssumption.do_primitive id prim typopt
- | VernacComments l -> unsupported_attributes atts;
- Flags.if_verbose Feedback.msg_info (str "Comments ok\n")
+ Feedback.msg_notice @@ vernac_locate ~pstate l;
+ pstate
+ | VernacRegister (qid, r) ->
+ unsupported_attributes atts;
+ vernac_register ~pstate qid r;
+ pstate
+ | VernacPrimitive (id, prim, typopt) ->
+ unsupported_attributes atts;
+ ComAssumption.do_primitive id prim typopt;
+ pstate
+ | VernacComments l ->
+ unsupported_attributes atts;
+ Flags.if_verbose Feedback.msg_info (str "Comments ok\n");
+ pstate
(* Proof management *)
- | VernacFocus n -> unsupported_attributes atts; vernac_focus n
- | VernacUnfocus -> unsupported_attributes atts; vernac_unfocus ()
- | VernacUnfocused -> unsupported_attributes atts;
- Feedback.msg_notice @@ vernac_unfocused ()
- | VernacBullet b -> unsupported_attributes atts; vernac_bullet b
- | VernacSubproof n -> unsupported_attributes atts; vernac_subproof n
- | VernacEndSubproof -> unsupported_attributes atts; vernac_end_subproof ()
- | VernacShow s -> unsupported_attributes atts;
- Feedback.msg_notice @@ vernac_show s
- | VernacCheckGuard -> unsupported_attributes atts;
- Feedback.msg_notice @@ vernac_check_guard ()
- | VernacProof (tac, using) -> unsupported_attributes atts;
+ | VernacFocus n ->
+ unsupported_attributes atts;
+ Option.map (vernac_focus n) pstate
+ | VernacUnfocus ->
+ unsupported_attributes atts;
+ Option.map (vernac_unfocus ()) pstate
+ | VernacUnfocused ->
+ unsupported_attributes atts;
+ Option.iter (fun pstate -> Feedback.msg_notice @@ vernac_unfocused ~pstate) pstate;
+ pstate
+ | VernacBullet b ->
+ unsupported_attributes atts;
+ Option.map (vernac_bullet b) pstate
+ | VernacSubproof n ->
+ unsupported_attributes atts;
+ Option.map (vernac_subproof n) pstate
+ | VernacEndSubproof ->
+ unsupported_attributes atts;
+ Option.map (vernac_end_subproof ()) pstate
+ | VernacShow s ->
+ unsupported_attributes atts;
+ Feedback.msg_notice @@ vernac_show ~pstate s;
+ pstate
+ | VernacCheckGuard ->
+ unsupported_attributes atts;
+ Feedback.msg_notice @@
+ vernac_require_open_proof ~pstate (vernac_check_guard);
+ pstate
+ | VernacProof (tac, using) ->
+ unsupported_attributes atts;
let using = Option.append using (Proof_using.get_default_proof_using ()) in
let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in
let usings = if Option.is_empty using then "using:no" else "using:yes" in
Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings);
- Option.iter vernac_set_end_tac tac;
- Option.iter vernac_set_used_variables using
- | VernacProofMode mn -> unsupported_attributes atts; ()
+ let pstate =
+ vernac_require_open_proof ~pstate (fun ~pstate ->
+ let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in
+ Option.cata (vernac_set_used_variables ~pstate) pstate using)
+ in Some pstate
+ | VernacProofMode mn ->
+ unsupported_attributes atts;
+ pstate
(* Extensions *)
| VernacExtend (opn,args) ->
(* XXX: Here we are returning the state! :) *)
- let _st : Vernacstate.t = Vernacextend.call ~atts opn args ~st in
- ()
+ let st : Vernacstate.t = Vernacextend.call ~atts opn args ~st in
+ st.Vernacstate.proof
(** A global default timeout, controlled by option "Set Default Timeout n".
Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
@@ -2333,12 +2557,18 @@ let () =
let current_timeout = ref None
-let vernac_timeout f =
+let vernac_timeout (f : 'a -> 'b) (x : 'a) : 'b =
match !current_timeout, !default_timeout with
- | Some n, _ | None, Some n ->
- let f () = f (); current_timeout := None in
- Control.timeout n f () Timeout
- | None, None -> f ()
+ | Some n, _
+ | None, Some n ->
+ let f v =
+ let res = f v in
+ current_timeout := None;
+ res
+ in
+ Control.timeout n f x Timeout
+ | None, None ->
+ f x
let restore_timeout () = current_timeout := None
@@ -2354,14 +2584,14 @@ let test_mode = ref false
(* XXX STATE: this type hints that restoring the state should be the
caller's responsibility *)
-let with_fail st b f =
+let with_fail ~st b f =
if not b
then f ()
else begin try
(* If the command actually works, ignore its effects on the state.
* Note that error has to be printed in the right state, hence
* within the purified function *)
- try f (); raise HasNotFailed
+ try ignore (f ()); raise HasNotFailed
with
| HasNotFailed as e -> raise e
| e ->
@@ -2378,60 +2608,66 @@ let with_fail st b f =
user_err ~hdr:"Fail" (str "The command has not failed!")
| HasFailed msg ->
if not !Flags.quiet || !test_mode then Feedback.msg_info
- (str "The command has indeed failed with message:" ++ fnl () ++ msg)
+ (str "The command has indeed failed with message:" ++ fnl () ++ msg);
+ st.Vernacstate.proof
| _ -> assert false
end
-let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
- let rec control = function
+let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} : Proof_global.t option =
+ let rec control ~st = function
| VernacExpr (atts, v) ->
- aux ~atts v
- | VernacFail v -> with_fail st true (fun () -> control v)
+ aux ~atts ~st v
+ | VernacFail v ->
+ with_fail ~st true (fun () -> control ~st v)
| VernacTimeout (n,v) ->
current_timeout := Some n;
- control v
+ control ~st v
| VernacRedirect (s, {v}) ->
- Topfmt.with_output_to_file s control v
- | VernacTime (batch, com) ->
+ Topfmt.with_output_to_file s (control ~st) v
+ | VernacTime (batch, ({v} as com)) ->
let header = if batch then Topfmt.pr_cmd_header com else Pp.mt () in
- System.with_time ~batch ~header control com.CAst.v;
+ System.with_time ~batch ~header (control ~st) v;
- and aux ~atts : _ -> unit =
+ and aux ~atts ~st : _ -> Proof_global.t option =
function
| VernacLoad (_,fname) ->
unsupported_attributes atts;
- vernac_load control fname
+ vernac_load ~st control fname
| c ->
(* NB: we keep polymorphism and program in the attributes, we're
just parsing them to do our option magic. *)
try
- vernac_timeout begin fun () ->
- if verbosely
- then Flags.verbosely (interp ?proof ~atts ~st) c
- else Flags.silently (interp ?proof ~atts ~st) c;
- end
- with
- | reraise when
- (match reraise with
- | Timeout -> true
- | e -> CErrors.noncritical e)
- ->
- let e = CErrors.push reraise in
- let e = locate_if_not_already ?loc e in
- let () = restore_timeout () in
- iraise e
+ vernac_timeout begin fun st ->
+ let pstate : Proof_global.t option =
+ if verbosely
+ then Flags.verbosely (interp ?proof ~atts ~st) c
+ else Flags.silently (interp ?proof ~atts ~st) c
+ in
+ pstate
+ end st
+ with
+ | reraise when
+ (match reraise with
+ | Timeout -> true
+ | e -> CErrors.noncritical e)
+ ->
+ let e = CErrors.push reraise in
+ let e = locate_if_not_already ?loc e in
+ let () = restore_timeout () in
+ iraise e
in
if verbosely
- then Flags.verbosely control c
- else control c
+ then Flags.verbosely (control ~st) c
+ else (control ~st) c
(* Be careful with the cache here in case of an exception. *)
let interp ?verbosely ?proof ~st cmd =
Vernacstate.unfreeze_interp_state st;
try
- interp ?verbosely ?proof ~st cmd;
+ let pstate = interp ?verbosely ?proof ~st cmd in
+ Vernacstate.Proof_global.set pstate;
Vernacstate.freeze_interp_state ~marshallable:false
with exn ->
let exn = CErrors.push exn in
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index f43cec48e9..2e6477995a 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -35,13 +35,16 @@ val make_cases : string -> string list list
(* XXX STATE: this type hints that restoring the state should be the
caller's responsibility *)
-val with_fail : Vernacstate.t -> bool -> (unit -> unit) -> unit
+val with_fail : st:Vernacstate.t -> bool -> (unit -> Proof_global.t option) -> Proof_global.t option
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.t option -> (pstate:Proof_global.t -> 'a) -> 'a
+
(* 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/vernacstate.ml b/vernac/vernacstate.ml
index c691dc8559..01c7068f33 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -28,10 +28,10 @@ module Parser = struct
end
type t = {
- parsing: Parser.state;
- system : States.state; (* summary + libstack *)
- proof : Proof_global.t; (* proof state *)
- shallow : bool; (* is the state trimmed down (libstack) *)
+ parsing : Parser.state;
+ system : States.state; (* summary + libstack *)
+ proof : Proof_global.t option; (* proof state *)
+ shallow : bool (* is the state trimmed down (libstack) *)
}
let s_cache = ref None
@@ -55,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 = update_cache s_proof (Proof_global.freeze ~marshallable);
+ proof = !s_proof;
shallow = false;
parsing = Parser.cur_state ();
}
let unfreeze_interp_state { system; proof; parsing } =
do_if_not_cached s_cache States.unfreeze system;
- do_if_not_cached s_proof Proof_global.unfreeze proof;
+ s_proof := proof;
Pcoq.unfreeze parsing
let make_shallow st =
@@ -71,3 +71,77 @@ let make_shallow st =
system = States.replace_lib st.system @@ Lib.drop_objects lib;
shallow = true;
}
+
+(* Compatibility module *)
+module Proof_global = struct
+
+ let with_fail ~st f = f ()
+
+ let get () = !s_proof
+ let set x = s_proof := x
+
+ let freeze ~marshallable:_ = get ()
+ let unfreeze x = s_proof := Some x
+
+ exception NoCurrentProof
+
+ let () =
+ CErrors.register_handler begin function
+ | NoCurrentProof ->
+ CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).")
+ | _ -> raise CErrors.Unhandled
+ end
+
+ open Proof_global
+
+ let cc f = match !s_proof with
+ | None -> raise NoCurrentProof
+ | Some x -> f x
+
+ let dd f = match !s_proof with
+ | None -> raise NoCurrentProof
+ | Some x -> s_proof := Some (f x)
+
+ let there_are_pending_proofs () = !s_proof <> None
+ let get_open_goals () = cc 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 simple_with_current_proof f =
+ dd (simple_with_current_proof f)
+
+ let with_current_proof f =
+ let pf, res = cc (with_current_proof f) in
+ s_proof := Some pf; res
+
+ let install_state s = s_proof := Some s
+
+ let return_proof ?allow_partial () =
+ cc (return_proof ?allow_partial)
+
+ let close_future_proof ~opaque ~feedback_id pf =
+ cc (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)
+
+ let discard_all () = s_proof := None
+ let update_global_env () = dd update_global_env
+
+ let get_current_context () = cc Pfedit.get_current_context
+
+ let get_all_proof_names () =
+ try cc get_all_proof_names
+ with NoCurrentProof -> []
+
+ let copy_terminators ~src ~tgt =
+ match src, tgt with
+ | None, None -> None
+ | Some _ , None -> None
+ | None, Some x -> Some x
+ | Some src, Some tgt -> Some (copy_terminators ~src ~tgt)
+
+end
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 581c23386a..42a87cfbd0 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -19,10 +19,10 @@ module Parser : sig
end
type t = {
- parsing: Parser.state;
- system : States.state; (* summary + libstack *)
- proof : Proof_global.t; (* proof state *)
- shallow : bool; (* is the state trimmed down (libstack) *)
+ parsing : Parser.state;
+ system : States.state; (* summary + libstack *)
+ proof : Proof_global.t option; (* proof state *)
+ shallow : bool (* is the state trimmed down (libstack) *)
}
val freeze_interp_state : marshallable:bool -> t
@@ -32,3 +32,55 @@ val make_shallow : t -> t
(* WARNING: Do not use, it will go away in future releases *)
val invalidate_cache : unit -> unit
+
+(* Compatibility module: Do Not Use *)
+module Proof_global : sig
+
+ val with_fail : st:t -> (unit -> unit) -> unit
+
+ open Proof_global
+
+ (* Low-level stuff *)
+ val get : unit -> t option
+ val set : t option -> unit
+
+ val freeze : marshallable:bool -> t option
+ val unfreeze : t -> 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 with_current_proof :
+ (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
+
+ val install_state : t -> unit
+
+ val return_proof : ?allow_partial:bool -> unit -> closed_proof_output
+
+ val close_future_proof :
+ opaque:opacity_flag ->
+ feedback_id:Stateid.t ->
+ closed_proof_output Future.computation -> closed_proof
+
+ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
+
+ val discard_all : unit -> unit
+ val update_global_env : unit -> unit
+
+ val get_current_context : unit -> Evd.evar_map * Environ.env
+
+ val get_all_proof_names : unit -> Names.Id.t list
+
+ val copy_terminators : src:t option -> tgt:t option -> t option
+
+end
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:29:28 +0000