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.

---
 doc/plugin_tutorial/tuto1/src/simple_check.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/plugin_tutorial')

diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml
index 1f636c531a..2949adde73 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_check.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml
@@ -6,7 +6,7 @@ let simple_check1 value_with_constraints =
 (* The point of renaming is to make sure the bound names printed by Check
    can be re-used in `apply with` tactics that use bound names to
    refer to arguments. *)
-    let j = Termops.on_judgment EConstr.of_constr
+    let j = Environ.on_judgment EConstr.of_constr
       (Arguments_renaming.rename_typing (Global.env())
          (EConstr.to_constr evd evalue)) in
     let {Environ.uj_type=x}=j in x
-- 
cgit v1.2.3