Merge PR #10304: Clean up tuto0 and tuto1 to use better practices and explain more

Ack-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot
Ack-by: tlringer

1 files changed, 10 insertions, 28 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml
index c2f09c64e0..684864a056 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_check.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml
@@ -1,32 +1,14 @@
-let simple_check1 value_with_constraints =
-  begin
-    let evalue, st = value_with_constraints 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 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 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,
+let simple_check1 env sigma evalue =
+(* This version should be preferred if 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()) sigma evalue
+  Typing.type_of env sigma evalue
 
-let simple_check3 value_with_constraints =
-  let evalue, st = value_with_constraints 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()) sigma evalue
+let simple_check2 env sigma evalue =
+(* This version should be preferred if 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 env sigma evalue