diff options
| author | Pierre-Marie Pédrot | 2020-04-30 16:05:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-03 13:09:49 +0200 |
| commit | 6839a2c9b7d2480e21572a7d176dcd6ea0617159 (patch) | |
| tree | cd0840fd07b436567f76924e2fcf219595194786 | |
| parent | 1109581ba7afca804515fc6179565da808bae4f7 (diff) | |
Remove a very specific low-level tactical from Refiner.
It was only used at one point in the STM, and its localization was suprising
to say the least. Furthermore it was relying on legacy code. Instead we hardcode
it in the STM.
| -rw-r--r-- | proofs/refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/refiner.mli | 1 | ||||
| -rw-r--r-- | stm/stm.ml | 6 |
3 files changed, 5 insertions, 4 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 6a0ba30bbf..ad84afd47e 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -271,5 +271,3 @@ let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} -let tclPUSHEVARUNIVCONTEXT ctx gl = - tclEVARS (Evd.merge_universe_context (project gl) ctx) gl diff --git a/proofs/refiner.mli b/proofs/refiner.mli index d4f2239a59..3471f38e9e 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -32,7 +32,6 @@ val tclIDTAC_MESSAGE : Pp.t -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic -val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies diff --git a/stm/stm.ml b/stm/stm.ml index f3768e9b99..5790bfc07e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2023,12 +2023,16 @@ end = struct (* {{{ *) match Future.join f with | Some (pt, uc) -> let sigma, env = PG_compat.get_current_context () in + let push_state ctx = + Proofview.tclEVARMAP >>= fun sigma -> + Proofview.Unsafe.tclEVARS (Evd.merge_universe_context sigma ctx) + in stm_pperr_endline (fun () -> hov 0 ( str"g=" ++ int (Evar.repr gid) ++ spc () ++ str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++ str"uc=" ++ Termops.pr_evar_universe_context uc)); (if abstract then Abstract.tclABSTRACT None else (fun x -> x)) - (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*> + (push_state uc <*> Tactics.exact_no_check (EConstr.of_constr pt)) | None -> if solve then Tacticals.New.tclSOLVE [] else tclUNIT () |