diff options
| author | Yves Bertot | 2018-05-04 09:12:06 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-04 09:12:06 +0200 |
| commit | 673f55be2b5139f154bbd84e72550a7c7c58341a (patch) | |
| tree | eb99108b50cf88f0fc33680f3c967fc2282132c1 | |
| parent | 93273e29708ff5c24024bde0e4b9955cb94a0dc0 (diff) | |
This revision contains a simple Check command.
| -rw-r--r-- | tuto1/_CoqProject | 2 | ||||
| -rw-r--r-- | tuto1/src/g_tuto1.ml4 | 11 | ||||
| -rw-r--r-- | tuto1/src/simple_check.ml | 9 | ||||
| -rw-r--r-- | tuto1/src/simple_check.mli | 1 | ||||
| -rw-r--r-- | tuto1/src/tuto1_plugin.mlpack | 1 |
5 files changed, 24 insertions, 0 deletions
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 |