3 files changed, 54 insertions, 4 deletions
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index 26a27b4c63..ff07a8f3d0 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -79,9 +79,29 @@ VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
 | [ "Cmd5" constr(e) ] ->
   [ 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
+    Feedback.msg_notice
+    (Termops.print_constr_env (Global.env()) evd
+       (Simple_check.simple_check1 v)) ]
+END
+
+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
+    Feedback.msg_notice
+      (Termops.print_constr_env (Global.env()) evd ty) ]
+END
+
+VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
+| [ "Cmd7" constr(e) ] ->
+  [ 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
       Feedback.msg_notice
       (Termops.print_constr_env (Global.env()) evd
-         (Simple_check.simple_check v)) ]
+         (Simple_check.simple_check3 v)) ]
 END
 \ No newline at end of file
diff --git a/tuto1/src/simple_check.ml b/tuto1/src/simple_check.ml
index 05be6632a0..e949e08a7c 100644
--- a/tuto1/src/simple_check.ml
+++ b/tuto1/src/simple_check.ml
@@ -1,9 +1,32 @@
-let simple_check value_with_constraints =
+let simple_check1 value_with_constraints =
   begin
     let evalue, st = value_with_constraints in
     let evd = 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 = Termops.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
-  end
-\ No newline at end of file
+  end
+
+let simple_check2 value_with_constraints =
+  let evalue, st = value_with_constraints in
+  let evd = 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
+
+let simple_check3 value_with_constraints =
+  let evalue, st = value_with_constraints in
+  let evd = 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
+\ No newline at end of file
diff --git a/tuto1/src/simple_check.mli b/tuto1/src/simple_check.mli
index d745e68f6d..7079ca925d 100644
--- a/tuto1/src/simple_check.mli
+++ b/tuto1/src/simple_check.mli
@@ -1 +1,8 @@
-val simple_check : EConstr.constr Evd.in_evar_universe_context -> EConstr.constr
-\ No newline at end of file
+val simple_check1 :
+  EConstr.constr Evd.in_evar_universe_context -> EConstr.constr
+
+val simple_check2 :
+  EConstr.constr Evd.in_evar_universe_context -> Evd.evar_map * EConstr.constr
+
+val simple_check3 :
+  EConstr.constr Evd.in_evar_universe_context -> EConstr.constr
+\ No newline at end of file