- 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).

1 files changed, 3 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