- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an evar_map

in tactics, avoiding useless and potentially costly merge's of constraints.
- Implement revert and generalize using the new tactics (not bound to syntax though,
as they are not backwards-compatible yet).

4 files changed, 9 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 83a703a3a9..6651e49652 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 dddf9b1c21..6177803c78 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 da9e8c68d6..157faae3dd 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 25ab1fb766..a74d8a46d3 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