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.

---
 pretyping/typing.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index e8d935fcbb..2e50e1ab3f 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -244,10 +244,10 @@ let judge_of_type u =
       uj_type = EConstr.mkType uu }
 
 let judge_of_relative env v =
-  Termops.on_judgment EConstr.of_constr (judge_of_relative env v)
+  Environ.on_judgment EConstr.of_constr (judge_of_relative env v)
 
 let judge_of_variable env id =
-  Termops.on_judgment EConstr.of_constr (judge_of_variable env id)
+  Environ.on_judgment EConstr.of_constr (judge_of_variable env id)
 
 let judge_of_projection env sigma p cj =
   let pty = lookup_projection p env in
@@ -307,7 +307,7 @@ let type_of_constructor env sigma ((ind,_ as ctor),u) =
   sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor)))
 
 let judge_of_int env v =
-  Termops.on_judgment EConstr.of_constr (judge_of_int env v)
+  Environ.on_judgment EConstr.of_constr (judge_of_int env v)
 
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
-- 
cgit v1.2.3