From 673f55be2b5139f154bbd84e72550a7c7c58341a Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 09:12:06 +0200
Subject: This revision contains a simple Check command.

---
 tuto1/_CoqProject             |  2 ++
 tuto1/src/g_tuto1.ml4         | 11 +++++++++++
 tuto1/src/simple_check.ml     |  9 +++++++++
 tuto1/src/simple_check.mli    |  1 +
 tuto1/src/tuto1_plugin.mlpack |  1 +
 5 files changed, 24 insertions(+)
 create mode 100644 tuto1/src/simple_check.ml
 create mode 100644 tuto1/src/simple_check.mli

diff --git a/tuto1/_CoqProject b/tuto1/_CoqProject
index 3f087e48d7..554893e739 100644
--- a/tuto1/_CoqProject
+++ b/tuto1/_CoqProject
@@ -1,6 +1,8 @@
 -R theories Tuto1
 -I src
 
+src/simple_check.mli
+src/simple_check.ml
 src/simple_declare.mli
 src/simple_declare.ml
 src/g_tuto1.ml4
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index d00da08b2d..26a27b4c63 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -74,3 +74,14 @@ VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF
       (Evd.from_env (Global.env())) e in
     Simple_declare.packed_declare_definition i v ]
 END
+
+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 (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)) ]
+END
\ No newline at end of file
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
diff --git a/tuto1/src/simple_check.mli b/tuto1/src/simple_check.mli
new file mode 100644
index 0000000000..d745e68f6d
--- /dev/null
+++ b/tuto1/src/simple_check.mli
@@ -0,0 +1 @@
+val simple_check : EConstr.constr Evd.in_evar_universe_context -> EConstr.constr
\ No newline at end of file
diff --git a/tuto1/src/tuto1_plugin.mlpack b/tuto1/src/tuto1_plugin.mlpack
index 17a27da09e..ccb4b6a538 100644
--- a/tuto1/src/tuto1_plugin.mlpack
+++ b/tuto1/src/tuto1_plugin.mlpack
@@ -1,2 +1,3 @@
+Simple_check
 Simple_declare
 G_tuto1
\ No newline at end of file
-- 
cgit v1.2.3