2 files changed, 20 insertions, 21 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 1d0aca1caf..300d62285a 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
@@ -145,12 +145,11 @@ END
   it gives an error message that is basically impossible to understand. *)
 
 VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
-| ![ proof ] [ "Cmd9" ] ->
+| ![ proof_query ] [ "Cmd9" ] ->
   { fun ~pstate ->
-    Option.iter (fun (pstate : Proof_global.t) ->
-        let sigma, env = Pfedit.get_current_context pstate in
-        let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in
-        Feedback.msg_notice
-          (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) pstate;
-    pstate }
+    let sigma, env = Pfedit.get_current_context pstate in
+    let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in
+    Feedback.msg_notice
+      (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
+  }
 END
diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml
index 2949adde73..c2f09c64e0 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_check.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml
@@ -1,32 +1,32 @@
 let simple_check1 value_with_constraints =
   begin
     let evalue, st = value_with_constraints in
-    let evd = Evd.from_ctx st in
+    let sigma = Evd.from_ctx st in
 (* This is reverse engineered from vernacentries.ml *)
 (* 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 = Environ.on_judgment EConstr.of_constr
       (Arguments_renaming.rename_typing (Global.env())
-         (EConstr.to_constr evd evalue)) in
+         (EConstr.to_constr sigma evalue)) in
     let {Environ.uj_type=x}=j in x
   end
 
 let simple_check2 value_with_constraints =
   let evalue, st = value_with_constraints in
-  let evd = Evd.from_ctx st in
+  let sigma = Evd.from_ctx st in
 (* This version should be preferred if bound variable names are not so
   important, you want to really verify that the input is well-typed,
   and if you want to obtain the type. *)
 (* Note that the output value is a pair containing a new evar_map:
    typing will fill out blanks in the term by add evar bindings. *)
-  Typing.type_of (Global.env()) evd evalue
+  Typing.type_of (Global.env()) sigma evalue
 
 let simple_check3 value_with_constraints =
   let evalue, st = value_with_constraints in
-  let evd = Evd.from_ctx st in
+  let sigma = Evd.from_ctx st in
 (* This version should be preferred if bound variable names are not so
   important and you already expect the input to have been type-checked
   before.  Set ~lax to false if you want an anomaly to be raised in
   case of a type error.  Otherwise a ReTypeError exception is raised. *)
-  Retyping.get_type_of ~lax:true (Global.env()) evd evalue
+  Retyping.get_type_of ~lax:true (Global.env()) sigma evalue