From a3fbe76736340e964917e6fcb9899735adb75eaf Mon Sep 17 00:00:00 2001
From: Talia Ringer
Date: Mon, 3 Jun 2019 09:41:22 -0400
Subject: Update tutorial plugin to use sigma, in keeping with doc
 recommendations

---
 doc/plugin_tutorial/tuto1/src/g_tuto1.mlg | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'doc/plugin_tutorial/tuto1/src/g_tuto1.mlg')

diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 1d0aca1caf..75251d8e33 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -94,9 +94,9 @@ VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
   { let v = Constrintern.interp_constr (Global.env())
       (Evd.from_env (Global.env())) e in
     let (_, ctx) = v in
-    let evd = Evd.from_ctx ctx in
+    let sigma = Evd.from_ctx ctx in
     Feedback.msg_notice
-    (Printer.pr_econstr_env (Global.env()) evd
+    (Printer.pr_econstr_env (Global.env()) sigma
        (Simple_check.simple_check1 v)) }
 END
 
@@ -104,9 +104,9 @@ VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY
 | [ "Cmd6" constr(e) ] ->
   { let v = Constrintern.interp_constr (Global.env())
       (Evd.from_env (Global.env())) e in
-    let evd, ty = Simple_check.simple_check2 v in
+    let sigma, ty = Simple_check.simple_check2 v in
     Feedback.msg_notice
-      (Printer.pr_econstr_env (Global.env()) evd ty) }
+      (Printer.pr_econstr_env (Global.env()) sigma ty) }
 END
 
 VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
@@ -114,9 +114,9 @@ VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
   { let v = Constrintern.interp_constr (Global.env())
       (Evd.from_env (Global.env())) e in
     let (a, ctx) = v in
-    let evd = Evd.from_ctx ctx in
+    let sigma = Evd.from_ctx ctx in
       Feedback.msg_notice
-      (Printer.pr_econstr_env (Global.env()) evd
+      (Printer.pr_econstr_env (Global.env()) sigma
          (Simple_check.simple_check3 v)) }
 END
 
@@ -128,9 +128,9 @@ END
 VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY
 | [ "Cmd8" reference(r) ] ->
   { let env = Global.env() in
-    let evd = Evd.from_env env in
+    let sigma = Evd.from_env env in
     Feedback.msg_notice
-    (Printer.pr_econstr_env env evd
+    (Printer.pr_econstr_env env sigma
       (EConstr.of_constr
         (Simple_print.simple_body_access (Nametab.global r)))) }
 END
-- 
cgit v1.2.3