From ac7169182a970c33be2e33abd43be5bf19542e2c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 8 Feb 2019 16:10:46 +0100
Subject: Fix #9527: unknown evar in nonterminating [fix] error.

---
 kernel/environ.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/environ.ml')

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 =
-- 
cgit v1.2.3