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.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/environ.mli')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index a9e0717559..0df9b91c4a 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -317,6 +317,10 @@ type ('constr, 'types) punsafe_judgment = {
   uj_val : 'constr;
   uj_type : 'types }
 
+val on_judgment       : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
+val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+
 type unsafe_judgment = (constr, types) punsafe_judgment
 
 val make_judge : 'constr -> 'types -> ('constr, 'types) punsafe_judgment
-- 
cgit v1.2.3