diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 2 | ||||
| -rw-r--r-- | stm/lemmas.ml | 24 | ||||
| -rw-r--r-- | stm/lemmas.mli | 13 | ||||
| -rw-r--r-- | stm/stm.ml | 2 |
4 files changed, 29 insertions, 12 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index e3fb0b607a..e525031e63 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -297,7 +297,7 @@ module Make(T : Task) = struct let slave_feeder oc fb = Marshal.to_channel oc (RespFeedback fb) []; flush oc in Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); - Pp.log_via_feedback (); + Pp.log_via_feedback (fun msg -> Richpp.repr (Richpp.richpp_of_pp msg)); Universes.set_remote_new_univ_level (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; match unmarshal_more_data (Option.get !slave_ic) with diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 6c18326882..17a10ccbab 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -328,7 +328,8 @@ let check_exist = ) let universe_proof_terminator compute_guard hook = - let open Proof_global in function + let open Proof_global in + make_terminator begin function | Admitted (id,k,pe,ctx) -> admit (id,k,pe) (hook (Some ctx)) (); Pp.feedback Feedback.AddedAxiom @@ -346,12 +347,16 @@ let universe_proof_terminator compute_guard hook = save_anonymous_with_strength ~export_seff proof kind id end; check_exist exports + end let standard_proof_terminator compute_guard hook = universe_proof_terminator compute_guard (fun _ -> hook) -let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = - let terminator = standard_proof_terminator compute_guard hook in +let start_proof id kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = + let terminator = match terminator with + | None -> standard_proof_terminator compute_guard hook + | Some terminator -> terminator compute_guard hook + in let sign = match sign with | Some sign -> sign @@ -360,8 +365,11 @@ let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = !start_hook c; Pfedit.start_proof id kind sigma sign c ?init_tac terminator -let start_proof_univs id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = - let terminator = universe_proof_terminator compute_guard hook in +let start_proof_univs id kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = + let terminator = match terminator with + | None -> universe_proof_terminator compute_guard hook + | Some terminator -> terminator compute_guard hook + in let sign = match sign with | Some sign -> sign @@ -421,7 +429,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = let body,opaq = retrieve_first_recthm ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = Evd.evar_universe_context_set (*FIXME*) Univ.UContext.empty ctx in + let ctx = UState.context_set (*FIXME*) ctx in let body = Option.map norm body in List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in @@ -491,7 +499,7 @@ let save_proof ?proof = function | _ -> None in Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),universes) in - Proof_global.get_terminator() pe + Proof_global.apply_terminator (Proof_global.get_terminator ()) pe | Vernacexpr.Proved (is_opaque,idopt) -> let (proof_obj,terminator) = match proof with @@ -501,7 +509,7 @@ let save_proof ?proof = function in (* if the proof is given explicitly, nothing has to be deleted *) if Option.is_empty proof then Pfedit.delete_current_proof (); - terminator (Proof_global.Proved (is_opaque,idopt,proof_obj)) + Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj))) (* Miscellaneous *) diff --git a/stm/lemmas.mli b/stm/lemmas.mli index 6556aa2297..dca6afe19b 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -24,11 +24,15 @@ val call_hook : (** A hook start_proof calls on the type of the definition being started *) val set_start_hook : (types -> unit) -> unit -val start_proof : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types -> +val start_proof : Id.t -> goal_kind -> Evd.evar_map -> + ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> + ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> unit declaration_hook -> unit -val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types -> +val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> + ?terminator:(lemma_possible_guards -> (Proof_global.proof_universes option -> unit declaration_hook) -> Proof_global.proof_terminator) -> + ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> (Proof_global.proof_universes option -> unit declaration_hook) -> unit @@ -40,6 +44,11 @@ val start_proof_with_initialization : (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit +val universe_proof_terminator : + Proof_global.lemma_possible_guards -> + (Proof_global.proof_universes option -> unit declaration_hook) -> + Proof_global.proof_terminator + val standard_proof_terminator : Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator diff --git a/stm/stm.ml b/stm/stm.ml index 42be4fca71..0c0bdc8272 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -171,7 +171,7 @@ type visit = { step : step; next : Stateid.t } (* Parts of the system state that are morally part of the proof state *) let summary_pstate = [ Evarutil.meta_counter_summary_name; - Evarutil.evar_counter_summary_name; + Evd.evar_counter_summary_name; "program-tcc-table" ] type state = { system : States.state; |