diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-02 00:24:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-02 00:28:43 +0200 |
| commit | def03f31c1c639629e6bb07e266319bf6930f8fb (patch) | |
| tree | a49452925b94da614f06df0941892ea1af69ec58 /stm | |
| parent | 1ae74bfd16f00bea0de14299cace8b638f768a70 (diff) | |
| parent | af2df1ada04da94a41a400c637788db461a532d9 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 4 | ||||
| -rw-r--r-- | stm/lemmas.ml | 18 |
2 files changed, 17 insertions, 5 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 73a90f611..2d1f725ef 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -229,10 +229,8 @@ module Make(T : Task) = struct | (Die | TQueue.BeingDestroyed) -> giveback_exec_token (); kill proc; exit () | Sys_error _ | Invalid_argument _ | End_of_file -> - giveback_exec_token (); T.on_task_cancellation_or_expiration_or_slave_death !last_task; - kill proc; - exit () + giveback_exec_token (); kill proc; exit () end module Pool = WorkerPool.Make(Model) diff --git a/stm/lemmas.ml b/stm/lemmas.ml index fb2f0351d..b676f4f51 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -480,6 +480,18 @@ let start_proof_com kind thms hook = (* Saving a proof *) +let keep_admitted_vars = ref true + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "keep section variables in admitted proofs"; + optkey = ["Keep"; "Admitted"; "Variables"]; + optread = (fun () -> !keep_admitted_vars); + optwrite = (fun b -> keep_admitted_vars := b) } + let save_proof ?proof = function | Vernacexpr.Admitted -> let pe = @@ -493,7 +505,8 @@ let save_proof ?proof = function error "Admitted requires an explicit statement"; let typ = Option.get const_entry_type in let ctx = Evd.evar_context_universe_context (fst universes) in - Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes) + let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in + Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes) | None -> let pftree = Pfedit.get_pftreestate () in let id, k, typ = Pfedit.current_proof_statement () in @@ -502,7 +515,8 @@ let save_proof ?proof = function let pproofs, _univs = Proof_global.return_proof ~allow_partial:true () in let sec_vars = - match Pfedit.get_used_variables(), pproofs with + if not !keep_admitted_vars then None + else match Pfedit.get_used_variables(), pproofs with | Some _ as x, _ -> x | None, (pproof, _) :: _ -> let env = Global.env () in |