diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-05 20:07:37 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-05 20:07:37 +0100 |
| commit | 7ca0319268c2c6912e08c53deb742d5f7631e210 (patch) | |
| tree | 5c9613224ca234af907374485b6f2241303e23ee /stm | |
| parent | 5d26829704b2602ede45183cba54ab219e453c0e (diff) | |
| parent | e4a682e2f2c91fac47f55cd8619af2321b2e4c30 (diff) | |
Merge remote-tracking branch 'origin/v8.5' into trunk
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 5 | ||||
| -rw-r--r-- | stm/stm.ml | 19 |
2 files changed, 19 insertions, 5 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 863bab7cc..e0315dec5 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -123,8 +123,9 @@ module Make(T : Task) = struct "-async-proofs-worker-priority"; Flags.string_of_priority !Flags.async_proofs_worker_priority] | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl - | ("-async-proofs" |"-toploop" |"-vi2vo" |"-compile" - |"-load-vernac-source" |"-compile-verbose" + | ("-async-proofs" |"-toploop" |"-vi2vo" + |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv" + |"-compile" |"-compile-verbose" |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl -> set_slave_opt tl | x::tl -> x :: set_slave_opt tl in diff --git a/stm/stm.ml b/stm/stm.ml index 96f127aa2..e08f69a0e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1470,6 +1470,18 @@ end = struct (* {{{ *) try Reach.known_state ~cache:`No id; let t, uc = Future.purify (fun () -> + let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in + let g = Evd.find sigma0 r_goal in + if not ( + Evarutil.is_ground_term sigma0 Evd.(evar_concl g) && + List.for_all (fun (_,bo,ty) -> + Evarutil.is_ground_term sigma0 ty && + Option.cata (Evarutil.is_ground_term sigma0) true bo) + Evd.(evar_context g)) + then + Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^ + "goals only")) + else begin vernac_interp r_state_fb r_ast; let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with @@ -1478,9 +1490,10 @@ end = struct (* {{{ *) let t = Evarutil.nf_evar sigma t in if Evarutil.is_ground_term sigma t then t, Evd.evar_universe_context sigma - else Errors.errorlabstrm "Stm" (str"The solution is not ground")) - () in - RespBuiltSubProof (t,uc) + else Errors.errorlabstrm "Stm" (str"The solution is not ground") + end) () + in + RespBuiltSubProof (t,uc) with e when Errors.noncritical e -> RespError (Errors.print e) let name_of_task { t_name } = t_name |