Merge PR #8811: EConstr-aware functions to produce kernel entries

1 files changed, 12 insertions, 0 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 4e1636e321..69ee5223c4 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -50,6 +50,18 @@ let new_global evd x =
 (* Expanding/testing/exposing existential variables *)
 (****************************************************)
 
+let finalize ?abort_on_undefined_evars sigma f =
+  let sigma = minimize_universes sigma in
+  let uvars = ref Univ.LSet.empty in
+  let v = f (fun c ->
+      let varsc = EConstr.universes_of_constr sigma c in
+      let c = EConstr.to_constr ?abort_on_undefined_evars sigma c in
+      uvars := Univ.LSet.union !uvars varsc;
+      c)
+  in
+  let sigma = restrict_universe_context sigma !uvars in
+  sigma, v
+
 (* flush_and_check_evars fails if an existential is undefined *)
 
 exception Uninstantiated_evar of Evar.t