This revision contains a simple Check command.

1 files changed, 9 insertions, 0 deletions

diff --git a/tuto1/src/simple_check.ml b/tuto1/src/simple_check.ml
new file mode 100644
index 0000000000..05be6632a0
--- /dev/null
+++ b/tuto1/src/simple_check.ml
@@ -0,0 +1,9 @@
+let simple_check value_with_constraints =
+  begin
+    let evalue, st = value_with_constraints in
+    let evd = Evd.from_ctx st in
+    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