diff options
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/proofview.ml | 3 | ||||
-rw-r--r-- | proofs/proofview.mli | 3 | ||||
-rw-r--r-- | proofs/refiner.ml | 2 | ||||
-rw-r--r-- | proofs/refiner.mli | 1 |
4 files changed, 9 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 83a703a3a..6651e4965 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -682,6 +682,9 @@ module V82 = struct let tclEVARS evd = Proof.modify (fun ps -> { ps with solution = evd }) + let tclEVARUNIVCONTEXT ctx = + Proof.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) + let has_unresolved_evar pv = Evd.has_undefined pv.solution diff --git a/proofs/proofview.mli b/proofs/proofview.mli index dddf9b1c2..6177803c7 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -298,6 +298,9 @@ module V82 : sig val tclEVARS : Evd.evar_map -> unit tactic + (* Set the evar universe context *) + val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic + val has_unresolved_evar : proofview -> bool (* Main function in the implementation of Grab Existential Variables. diff --git a/proofs/refiner.ml b/proofs/refiner.ml index da9e8c68d..157faae3d 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -325,6 +325,8 @@ let rec tclREPEAT_MAIN t g = (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} +let tclEVARUNIVCONTEXT ctx gls = tclIDTAC {gls with sigma= Evd.set_universe_context gls.sigma ctx} + (* Push universe context *) let tclPUSHCONTEXT rigid ctx tac gl = tclTHEN (tclEVARS (Evd.merge_context_set rigid (project gl) ctx)) tac gl diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 25ab1fb76..a74d8a46d 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -33,6 +33,7 @@ val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic +val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic val tclPUSHCONTEXT : Evd.rigid -> Univ.universe_context_set -> tactic -> tactic val tclPUSHEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic |