Merge pull request #8778 from SkySkimmer/merge-plugin-tuto

Move plugin tutorial to Coq repo

1 files changed, 23 insertions, 0 deletions

diff --git a/doc/plugin_tutorial/tuto3/theories/test.v b/doc/plugin_tutorial/tuto3/theories/test.v
new file mode 100644
index 0000000000..43204ddf34
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/theories/test.v
@@ -0,0 +1,23 @@
+(* to be used e.g. in : coqtop -I src -R theories Tuto3 < theories/test.v *)
+
+Require Import Tuto3.Loader.
+
+(* This should print Type. *)
+Tuto3_1.
+
+(* This should print a term that contains an existential variable. *)
+(* And then print the same term, where the variable has been correctly
+   instantiated. *)
+Tuto3_2.
+
+Lemma tutu x y (A : 0 < x) (B : 10 < y) : True.
+Proof.
+pack hypothesis A.
+(* Hypothesis A should have disappeared and a "packed_hyps" hypothesis
+  should have appeared, with unreadable content. *)
+pack hypothesis B.
+(* Hypothesis B should have disappeared *)
+destruct packed_hyps as [unpacked_hyps].
+(* Hypothesis unpacked_hyps should contain the previous contents of A and B. *)
+exact I.
+Qed.