aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
diff options
context:
space:
mode:
authorJim Fehrle2019-06-03 14:36:52 -0700
committerJim Fehrle2019-06-03 14:36:52 -0700
commit3b87df6b55d9c1ed4a8f32ff6195540f870d7e25 (patch)
tree16eb5c39436b6b03dce93d897786fddc9faa9aa3 /doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
parent77fa4df223dc483ebf51fd34d82bb9d3d3405be4 (diff)
parenta18b1ae63e07cf7e174e3e8862ac32f00ce74865 (diff)
Merge branch 'master' of https://github.com/coq/coq
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/g_tuto1.mlg')
-rw-r--r--doc/plugin_tutorial/tuto1/src/g_tuto1.mlg16
1 files changed, 8 insertions, 8 deletions
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