Fix #9527: unknown evar in nonterminating [fix] error.

1 files changed, 4 insertions, 0 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 886d6b1feb..ab046f02f7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -682,6 +682,10 @@ type ('constr, 'types) punsafe_judgment = {
   uj_val : 'constr;
   uj_type : 'types }
 
+let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
+let on_judgment_value f j = { j with uj_val = f j.uj_val }
+let on_judgment_type f j = { j with uj_type = f j.uj_type }
+
 type unsafe_judgment = (constr, types) punsafe_judgment
 
 let make_judge v tj =