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.

---
 engine/termops.ml  | 8 +++-----
 engine/termops.mli | 3 +++
 2 files changed, 6 insertions(+), 5 deletions(-)

(limited to 'engine')

diff --git a/engine/termops.ml b/engine/termops.ml
index 579100ad4c..2f766afaa6 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1417,11 +1417,9 @@ let prod_applist_assum sigma n c l =
     | _ -> anomaly (Pp.str "Not enough prod/let's.") in
   app n [] c l
 
-(* Combinators on judgments *)
-
-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 }
+let on_judgment = Environ.on_judgment
+let on_judgment_value = Environ.on_judgment_value
+let on_judgment_type = Environ.on_judgment_type
 
 (* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in
      variables skips let-in's; let-in's in the middle are put in ctx2 *)
diff --git a/engine/termops.mli b/engine/termops.mli
index 61a6ec1cd6..dea59e9efc 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -295,8 +295,11 @@ val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
 (** Combinators on judgments *)
 
 val on_judgment       : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
+[@@ocaml.deprecated "Use [Environ.on_judgment]."]
 val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+[@@ocaml.deprecated "Use [Environ.on_judgment_value]."]
 val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+[@@ocaml.deprecated "Use [Environ.on_judgment_type]."]
 
 (** {5 Debug pretty-printers} *)
 
-- 
cgit v1.2.3