Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e40b'

git-subtree-dir: doc/plugin_tutorial
git-subtree-mainline: 8c040974facb733682d24c488dc89941671f4ab7
git-subtree-split: 168a13dab1c9987f592994150997e692d4d7e40b

44 files changed, 1445 insertions, 0 deletions

diff --git a/doc/plugin_tutorial/.gitignore b/doc/plugin_tutorial/.gitignore
new file mode 100644
index 0000000000..3e4978fac4
--- /dev/null
+++ b/doc/plugin_tutorial/.gitignore
@@ -0,0 +1,13 @@
+*.ml*.d
+*.cm[ixt]*
+Makefile.coq*
+*~
+*.[ao]
+.coqdeps.d
+*.vo
+*.glob
+*.aux
+*/*/.merlin
+
+# by convention g_foo.ml is generated
+g_*.ml
diff --git a/doc/plugin_tutorial/.travis.yml b/doc/plugin_tutorial/.travis.yml
new file mode 100644
index 0000000000..556e0ac45a
--- /dev/null
+++ b/doc/plugin_tutorial/.travis.yml
@@ -0,0 +1,38 @@
+dist: trusty
+sudo: required
+language: generic
+
+services:
+  - docker
+
+env:
+  global:
+  - NJOBS="2"
+  - CONTRIB_NAME="plugin_tutorials"
+  matrix:
+  - COQ_IMAGE="coqorg/coq:dev"
+
+install: |
+  # Prepare the COQ container
+  docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/$CONTRIB_NAME -w /home/coq/$CONTRIB_NAME ${COQ_IMAGE}
+  docker exec COQ /bin/bash --login -c "
+    # This bash script is double-quoted to interpolate Travis CI env vars:
+    echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\"
+    export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
+    set -ex  # -e = exit on failure; -x = trace for debug
+    opam list
+    "
+script:
+- echo -e "${ANSI_YELLOW}Building $CONTRIB_NAME...${ANSI_RESET}" && echo -en 'travis_fold:start:testbuild\\r'
+- |
+  docker exec COQ /bin/bash --login -c "
+    export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
+    set -ex
+    sudo chown -R coq:coq /home/coq/$CONTRIB_NAME
+    ( cd tuto0 && make )
+    ( cd tuto1 && make )
+    ( cd tuto2 && make )
+    ( cd tuto3 && make )
+    "
+- docker stop COQ  # optional
+- echo -en 'travis_fold:end:testbuild\\r'
diff --git a/doc/plugin_tutorial/LICENSE b/doc/plugin_tutorial/LICENSE
new file mode 100644
index 0000000000..cf1ab25da0
--- /dev/null
+++ b/doc/plugin_tutorial/LICENSE
@@ -0,0 +1,24 @@
+This is free and unencumbered software released into the public domain.
+
+Anyone is free to copy, modify, publish, use, compile, sell, or
+distribute this software, either in source code form or as a compiled
+binary, for any purpose, commercial or non-commercial, and by any
+means.
+
+In jurisdictions that recognize copyright laws, the author or authors
+of this software dedicate any and all copyright interest in the
+software to the public domain. We make this dedication for the benefit
+of the public at large and to the detriment of our heirs and
+successors. We intend this dedication to be an overt act of
+relinquishment in perpetuity of all present and future rights to this
+software under copyright law.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR
+OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
+ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+OTHER DEALINGS IN THE SOFTWARE.
+
+For more information, please refer to <http://unlicense.org>
diff --git a/doc/plugin_tutorial/README.md b/doc/plugin_tutorial/README.md
new file mode 100644
index 0000000000..f82edb2352
--- /dev/null
+++ b/doc/plugin_tutorial/README.md
@@ -0,0 +1,86 @@
+How to write plugins in Coq
+===========================
+  # Working environment : merlin, tuareg (open question)
+  
+  ## OCaml & related tools
+
+  These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html)
+
+```shell
+opam init --root=$PWD/CIW2018 --compiler=4.06.0 -j2
+eval `opam config env --root=$PWD/CIW2018`
+opam install camlp5 ocamlfind num # Coq's dependencies
+opam install lablgtk              # Coqide's dependencies (optional)
+opam install merlin               # prints instructions for vim and emacs
+```
+
+  ## Coq
+
+```shell
+git clone git@github.com:coq/coq.git
+cd coq
+./configure -profile devel
+make -j2
+cd ..
+export PATH=$PWD/coq/bin:$PATH
+```
+
+  ## This tutorial
+
+```shell
+git clone git@github.com:ybertot/plugin_tutorials.git
+cd plugin_tutorials/tuto0
+make .merlin                # run before opening .ml files in your editor
+make                        # build
+```
+  
+  
+  
+  # tuto0 : basics of project organization
+  package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject`
+  - Example of syntax to add a new toplevel command
+  - Example of function call to print a simple message
+  - Example of syntax to add a simple tactic
+      (that does nothing and prints a message)
+  - To use it:
+
+```bash
+    cd tuto0; make
+    coqtop -I src -R theories Tuto0
+```
+
+  In the Coq session type:
+```coq
+    Require Import Tuto0.Loader. HelloWorld.
+```
+
+  # tuto1 : Ocaml to Coq communication
+  Explore the memory of Coq, modify it
+  - Commands that take arguments: strings, symbols, expressions of the calculus of constructions
+  - Commands that interact with type-checking in Coq
+  - A command that adds a new definition or theorem
+  - A command that uses a name and exploits the existing definitions
+    or theorems
+  - A command that exploits an existing ongoing proof
+  - A command that defines a new tactic
+
+  Compilation and loading must be performed as for `tuto0`.
+  
+  # tuto2 : Ocaml to Coq communication
+  A more step by step introduction to writing commands
+  - Explanation of the syntax of entries
+  - Adding a new type to and parsing to the available choices
+  - Handling commands that store information in user-chosen registers and tables
+
+  Compilation and loading must be performed as for `tuto1`.
+
+  # tuto3 : manipulating terms of the calculus of constructions
+  Manipulating terms, inside commands and tactics.
+  - Obtaining existing values from memory
+  - Composing values
+  - Verifying types
+  - Using these terms in commands
+  - Using these terms in tactics
+  - Automatic proofs without tactics using type classes and canonical structures
+
+  compilation and loading must be performed as for `tuto0`.
diff --git a/doc/plugin_tutorial/tuto0/Makefile b/doc/plugin_tutorial/tuto0/Makefile
new file mode 100644
index 0000000000..e0e197650d
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/Makefile
@@ -0,0 +1,14 @@
+ifeq "$(COQBIN)" ""
+  COQBIN=$(dir $(shell which coqtop))/
+endif
+
+%: Makefile.coq
+
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+
+tests: all
+	@$(MAKE) -C tests -s clean
+	@$(MAKE) -C tests -s all
+
+-include Makefile.coq
diff --git a/doc/plugin_tutorial/tuto0/_CoqProject b/doc/plugin_tutorial/tuto0/_CoqProject
new file mode 100644
index 0000000000..76368e3ac7
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/_CoqProject
@@ -0,0 +1,10 @@
+-R theories/ Tuto0
+-I src
+
+theories/Loader.v
+theories/Demo.v
+
+src/tuto0_main.ml
+src/tuto0_main.mli
+src/g_tuto0.mlg
+src/tuto0_plugin.mlpack
diff --git a/doc/plugin_tutorial/tuto0/src/dune b/doc/plugin_tutorial/tuto0/src/dune
new file mode 100644
index 0000000000..79d561061d
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/src/dune
@@ -0,0 +1,9 @@
+(library
+ (name tuto0_plugin)
+ (public_name coq.plugins.tutorial.p0)
+ (libraries coq.plugins.ltac))
+
+(rule
+ (targets g_tuto0.ml)
+ (deps (:pp-file g_tuto0.mlg) )
+ (action (run coqpp %{pp-file})))
diff --git a/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg
new file mode 100644
index 0000000000..5c633fe862
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg
@@ -0,0 +1,18 @@
+DECLARE PLUGIN "tuto0_plugin"
+
+{
+
+open Pp
+open Ltac_plugin
+
+}
+
+VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
+| [ "HelloWorld" ] -> { Feedback.msg_notice (strbrk Tuto0_main.message) }
+END
+
+TACTIC EXTEND hello_world_tactic
+| [ "hello_world" ] ->
+  { let _ = Feedback.msg_notice (str Tuto0_main.message) in
+    Tacticals.New.tclIDTAC }
+END
diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_main.ml b/doc/plugin_tutorial/tuto0/src/tuto0_main.ml
new file mode 100644
index 0000000000..93a807a800
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/src/tuto0_main.ml
@@ -0,0 +1 @@
+let message = "Hello world!"
diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_main.mli b/doc/plugin_tutorial/tuto0/src/tuto0_main.mli
new file mode 100644
index 0000000000..846af3ed8c
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/src/tuto0_main.mli
@@ -0,0 +1 @@
+val message : string
diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack b/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack
new file mode 100644
index 0000000000..73be1bb561
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack
@@ -0,0 +1,2 @@
+Tuto0_main
+G_tuto0
diff --git a/doc/plugin_tutorial/tuto0/theories/Demo.v b/doc/plugin_tutorial/tuto0/theories/Demo.v
new file mode 100644
index 0000000000..bdc61986af
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/theories/Demo.v
@@ -0,0 +1,8 @@
+From Tuto0 Require Import Loader.
+
+HelloWorld.
+
+Lemma test : True.
+Proof.
+hello_world.
+Abort.
diff --git a/doc/plugin_tutorial/tuto0/theories/Loader.v b/doc/plugin_tutorial/tuto0/theories/Loader.v
new file mode 100644
index 0000000000..7bce38382b
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/theories/Loader.v
@@ -0,0 +1 @@
+Declare ML Module "tuto0_plugin".
diff --git a/doc/plugin_tutorial/tuto1/Makefile b/doc/plugin_tutorial/tuto1/Makefile
new file mode 100644
index 0000000000..e0e197650d
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/Makefile
@@ -0,0 +1,14 @@
+ifeq "$(COQBIN)" ""
+  COQBIN=$(dir $(shell which coqtop))/
+endif
+
+%: Makefile.coq
+
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+
+tests: all
+	@$(MAKE) -C tests -s clean
+	@$(MAKE) -C tests -s all
+
+-include Makefile.coq
diff --git a/doc/plugin_tutorial/tuto1/_CoqProject b/doc/plugin_tutorial/tuto1/_CoqProject
new file mode 100644
index 0000000000..585d1360be
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/_CoqProject
@@ -0,0 +1,13 @@
+-R theories Tuto1
+-I src
+
+theories/Loader.v
+
+src/simple_check.mli
+src/simple_check.ml
+src/simple_declare.mli
+src/simple_declare.ml
+src/simple_print.ml
+src/simple_print.mli
+src/g_tuto1.mlg
+src/tuto1_plugin.mlpack
diff --git a/doc/plugin_tutorial/tuto1/src/dune b/doc/plugin_tutorial/tuto1/src/dune
new file mode 100644
index 0000000000..cf9c674b14
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/dune
@@ -0,0 +1,9 @@
+(library
+ (name tuto1_plugin)
+ (public_name coq.plugins.tutorial.p1)
+ (libraries coq.plugins.ltac))
+
+(rule
+ (targets g_tuto1.ml)
+ (deps (:pp-file g_tuto1.mlg) )
+ (action (run coqpp %{pp-file})))
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
new file mode 100644
index 0000000000..4df284d2d9
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -0,0 +1,154 @@
+DECLARE PLUGIN "tuto1_plugin"
+
+{
+
+(* If we forget this line and include our own tactic definition using
+  TACTIC EXTEND, as below, then we get the strange error message
+  no implementation available for Tacentries, only when compiling
+  theories/Loader.v
+*)
+open Ltac_plugin
+open Attributes
+open Pp
+(* This module defines the types of arguments to be used in the
+   EXTEND directives below, for example the string one. *)
+open Stdarg
+
+}
+
+VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
+| [ "Hello" string(s) ] ->
+  { Feedback.msg_notice (strbrk "Hello " ++ str s) }
+END
+
+(* reference is allowed as a syntactic entry, but so are all the entries
+   found the signature of module Prim in file coq/parsing/pcoq.mli *)
+
+VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY
+| [ "HelloAgain" reference(r)] ->
+(* The function Ppconstr.pr_qualid was found by searching all mli files
+   for a function of type qualid -> Pp.t *)
+  { Feedback.msg_notice
+      (strbrk "Hello again " ++ Ppconstr.pr_qualid r)}
+END
+
+(* According to parsing/pcoq.mli, e has type constr_expr *)
+(* this type is defined in pretyping/constrexpr.ml *)
+(* Question for the developers: why is the file constrexpr.ml and not
+   constrexpr.mli --> Easier for packing the software in components. *)
+VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY
+| [ "Cmd1" constr(e) ] ->
+  { let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") }
+END
+
+(* The next step is to make something of parsed expression.
+   Interesting information in interp/constrintern.mli *)
+
+(* There are several phases of transforming a parsed expression into
+  the final internal data-type (constr).  There exists a collection of
+  functions that combine all the phases *)
+
+VERNAC COMMAND EXTEND TakingConstr2 CLASSIFIED AS QUERY
+| [ "Cmd2" constr(e) ] ->
+  { let _ = Constrintern.interp_constr
+    (Global.env())
+    (* Make sure you don't use Evd.empty here, as this does not
+      check consistency with existing universe constraints. *)
+    (Evd.from_env (Global.env())) e in
+    Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") }
+END
+
+(* This is to show what happens when typing in an empty environment
+  with an empty evd.
+ Question for the developers: why does "Cmd3 (fun x : nat => x)."
+ raise an anomaly, not the same error as "Cmd3 (fun x : a => x)." *)
+ 
+VERNAC COMMAND EXTEND TakingConstr3 CLASSIFIED AS QUERY
+| [ "Cmd3" constr(e) ] ->
+  { let _ = Constrintern.interp_constr Environ.empty_env
+      Evd.empty e in
+      Feedback.msg_notice
+        (strbrk "Cmd3 accepted something in the empty context")}
+END
+
+(* When adding a definition, we have to be careful that just
+  the operation of constructing a well-typed term may already change
+  the environment, at the level of universe constraints (which
+  are recorded in the evd component).  The function
+  Constrintern.interp_constr ignores this side-effect, so it should
+  not be used here. *)
+
+(* Looking at the interface file interp/constrintern.ml4, I lost
+  some time because I did not see that the "constr" type appearing
+  there was "EConstr.constr" and not "Constr.constr". *)
+
+VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF
+| #[ poly = polymorphic ] [ "Cmd4" ident(i) constr(e) ] ->
+  { let v = Constrintern.interp_constr (Global.env())
+      (Evd.from_env (Global.env())) e in
+    Simple_declare.packed_declare_definition ~poly 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 (_, ctx) = v in
+    let evd = Evd.from_ctx ctx in
+    Feedback.msg_notice
+    (Printer.pr_econstr_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
+      (Printer.pr_econstr_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
+      (Printer.pr_econstr_env (Global.env()) evd
+         (Simple_check.simple_check3 v)) }
+END
+
+(* This command takes a name and return its value.  It does less
+  than Print, because it fails on constructors, axioms, and inductive types.
+  This should be improved, because the error message is an anomaly.
+  Anomalies should never appear even when using a command outside of its
+  intended use. *)
+VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY
+| [ "Cmd8" reference(r) ] ->
+  { let env = Global.env() in
+    let evd = Evd.from_env env in
+    Feedback.msg_notice
+    (Printer.pr_econstr_env env evd
+      (EConstr.of_constr
+        (Simple_print.simple_body_access (Nametab.global r)))) }
+END
+
+TACTIC EXTEND my_intro
+| [ "my_intro" ident(i) ] ->
+  { Tactics.introduction i }
+END
+
+(* if one write this:
+  VERNAC COMMAND EXTEND exploreproof CLASSIFIED AS QUERY
+  it gives an error message that is basically impossible to understand. *)
+
+VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
+| [ "Cmd9" ] ->
+  { let p = Proof_global.give_me_the_proof () in
+    let sigma, env = Pfedit.get_current_context () in
+    let pprf = Proof.partial_proof p in
+    Feedback.msg_notice
+      (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) }
+END
diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml
new file mode 100644
index 0000000000..1f636c531a
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml
@@ -0,0 +1,32 @@
+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
+
+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
diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.mli b/doc/plugin_tutorial/tuto1/src/simple_check.mli
new file mode 100644
index 0000000000..bcf1bf56cf
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/simple_check.mli
@@ -0,0 +1,8 @@
+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
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
new file mode 100644
index 0000000000..9d10a8ba72
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -0,0 +1,24 @@
+(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *)
+let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
+  let sigma = Evd.minimize_universes sigma in
+  let body = EConstr.to_constr sigma body in
+  let tyopt = Option.map (EConstr.to_constr sigma) tyopt in
+  let uvars_fold uvars c =
+    Univ.LSet.union uvars (Vars.universes_of_constr c) in
+  let uvars = List.fold_left uvars_fold Univ.LSet.empty
+     (Option.List.cons tyopt [body]) in
+  let sigma = Evd.restrict_universe_context sigma uvars in
+  let univs = Evd.check_univ_decl ~poly sigma udecl in
+  let ubinders = Evd.universe_binders sigma in
+  let ce = Declare.definition_entry ?types:tyopt ~univs body in
+  DeclareDef.declare_definition ident k ce ubinders imps ~hook
+
+let packed_declare_definition ~poly ident value_with_constraints =
+  let body, ctx = value_with_constraints in
+  let sigma = Evd.from_ctx ctx in
+  let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in
+  let udecl = UState.default_univ_decl in
+  let nohook = Lemmas.mk_hook (fun _ x -> ()) in
+  ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
+
+(* But this definition cannot be undone by Reset ident *)
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.mli b/doc/plugin_tutorial/tuto1/src/simple_declare.mli
new file mode 100644
index 0000000000..fd74e81526
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.mli
@@ -0,0 +1,5 @@
+open Names
+open EConstr
+
+val packed_declare_definition :
+    poly:bool -> Id.t -> constr Evd.in_evar_universe_context -> unit
diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml
new file mode 100644
index 0000000000..cfc38ff9c9
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml
@@ -0,0 +1,17 @@
+(* A more advanced example of how to explore the structure of terms of
+  type constr is given in the coq-dpdgraph plugin. *)
+
+let simple_body_access gref =
+  match gref with
+  | Globnames.VarRef _ ->
+    failwith "variables are not covered in this example"
+  | Globnames.IndRef _ ->
+    failwith "inductive types are not covered in this example"
+  | Globnames.ConstructRef _ ->
+    failwith "constructors are not covered in this example"
+  | Globnames.ConstRef cst ->
+    let cb = Environ.lookup_constant cst (Global.env()) in
+    match Global.body_of_constant_body cb with
+    | Some(e, _) -> e
+    | None -> failwith "This term has no value"
+
diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.mli b/doc/plugin_tutorial/tuto1/src/simple_print.mli
new file mode 100644
index 0000000000..254b56ff79
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/simple_print.mli
@@ -0,0 +1 @@
+val simple_body_access : Names.GlobRef.t -> Constr.constr
diff --git a/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack
new file mode 100644
index 0000000000..a797a509e0
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack
@@ -0,0 +1,4 @@
+Simple_check
+Simple_declare
+Simple_print
+G_tuto1
diff --git a/doc/plugin_tutorial/tuto1/theories/Loader.v b/doc/plugin_tutorial/tuto1/theories/Loader.v
new file mode 100644
index 0000000000..6e8e308b3f
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/theories/Loader.v
@@ -0,0 +1 @@
+Declare ML Module "tuto1_plugin".
diff --git a/doc/plugin_tutorial/tuto2/Makefile b/doc/plugin_tutorial/tuto2/Makefile
new file mode 100644
index 0000000000..e0e197650d
--- /dev/null
+++ b/doc/plugin_tutorial/tuto2/Makefile
@@ -0,0 +1,14 @@
+ifeq "$(COQBIN)" ""
+  COQBIN=$(dir $(shell which coqtop))/
+endif
+
+%: Makefile.coq
+
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+
+tests: all
+	@$(MAKE) -C tests -s clean
+	@$(MAKE) -C tests -s all
+
+-include Makefile.coq
diff --git a/doc/plugin_tutorial/tuto2/_CoqProject b/doc/plugin_tutorial/tuto2/_CoqProject
new file mode 100644
index 0000000000..cf9cb5cc26
--- /dev/null
+++ b/doc/plugin_tutorial/tuto2/_CoqProject
@@ -0,0 +1,6 @@
+-R theories/ Tuto
+-I src
+
+theories/Test.v
+src/demo.mlg
+src/demo_plugin.mlpack
diff --git a/doc/plugin_tutorial/tuto2/src/.gitignore b/doc/plugin_tutorial/tuto2/src/.gitignore
new file mode 100644
index 0000000000..5b1b6a902e
--- /dev/null
+++ b/doc/plugin_tutorial/tuto2/src/.gitignore
@@ -0,0 +1 @@
+/demo.ml
diff --git a/doc/plugin_tutorial/tuto2/src/demo.mlg b/doc/plugin_tutorial/tuto2/src/demo.mlg
new file mode 100644
index 0000000000..966c05acdc
--- /dev/null
+++ b/doc/plugin_tutorial/tuto2/src/demo.mlg
@@ -0,0 +1,375 @@
+(* -------------------------------------------------------------------------- *)
+(*                                                                            *)
+(*                            Initial ritual dance                            *)
+(*                                                                            *)
+(* -------------------------------------------------------------------------- *)
+
+DECLARE PLUGIN "demo_plugin"
+
+(*
+   Use this macro before any of the other OCaml macros.
+
+   Each plugin has a unique name.
+   We have decided to name this plugin as "demo_plugin".
+   That means that:
+   
+   (1) If we want to load this particular plugin to Coq toplevel,
+       we must use the following command.
+
+         Declare ML Module "demo_plugin".
+
+   (2) The above command will succeed only if there is "demo_plugin.cmxs"
+       in some of the directories that Coq is supposed to look
+       (i.e. the ones we specified via "-I ..." command line options).
+
+   (3) The file "demo_plugin.mlpack" lists the OCaml modules to be linked in
+       "demo_plugin.cmxs".
+
+   (4) The file "demo_plugin.mlpack" as well as all .ml, .mli and .mlg files
+       are listed in the "_CoqProject" file.
+*)
+
+(* -------------------------------------------------------------------------- *)
+(*                                                                            *)
+(*                 How to define a new Vernacular command?                    *)
+(*                                                                            *)
+(* -------------------------------------------------------------------------- *)
+
+VERNAC COMMAND EXTEND Cmd1 CLASSIFIED AS QUERY
+| [ "Cmd1" ] -> { () }
+END
+
+(*
+   These:
+
+     VERNAC COMMAND EXTEND
+
+   and
+
+     END
+
+   mark the beginning and the end of the definition of a new Vernacular command.
+
+   Cmd1 is a unique identifier (which must start with an upper-case letter)
+   associated with the new Vernacular command we are defining.
+
+   CLASSIFIED AS QUERY tells Coq that the new Vernacular command:
+   - changes neither the global environment
+   - nor does it modify the plugin's state.
+
+   If the new command could:
+   - change the global environment
+   - or modify a plugin's state
+   then one would have to use CLASSIFIED AS SIDEFF instead.
+
+   This:
+
+     [ "Cmd1" ] -> { () }
+
+   defines:
+   - the parsing rule
+   - the interpretation rule
+
+   The parsing rule and the interpretation rule are separated by -> token.
+
+   The parsing rule, in this case, is:
+
+     [ "Cmd1" ]
+
+   By convention, all vernacular command start with an upper-case letter.
+
+   The [ and ] characters mark the beginning and the end of the parsing rule.
+   The parsing rule itself says that the syntax of the newly defined command
+   is composed from a single terminal Cmd1.
+   
+   The interpretation rule, in this case, is:
+
+     { () }
+
+   Similarly to the case of the parsing rule,
+   { and } characters mark the beginning and the end of the interpretation rule.
+   In this case, the following Ocaml expression:
+
+     ()
+
+   defines the effect of the Vernacular command we have just defined.
+   That is, it behaves is no-op.
+*)
+
+(* -------------------------------------------------------------------------- *)
+(*                                                                            *)
+(*   How to define a new Vernacular command with some terminal parameters?    *)
+(*                                                                            *)
+(* -------------------------------------------------------------------------- *)
+
+VERNAC COMMAND EXTEND Cmd2 CLASSIFIED AS QUERY
+| [ "Cmd2" "With" "Some" "Terminal" "Parameters" ] -> { () }
+END
+
+(*
+   As shown above, the Vernacular command can be composed from
+   any number of terminals.
+
+   By convention, each of these terminals starts with an upper-case letter.
+*)
+
+(* -------------------------------------------------------------------------- *)
+(*                                                                            *)
+(*  How to define a new Vernacular command with some non-terminal parameter?  *)
+(*                                                                            *)
+(* -------------------------------------------------------------------------- *)
+
+{
+
+open Stdarg
+
+}
+
+VERNAC COMMAND EXTEND Cmd3 CLASSIFIED AS QUERY
+| [ "Cmd3" int(i) ] -> { () }
+END
+
+(*
+   This:
+
+     open Stdarg
+
+   is needed as some identifiers in the Ocaml code generated by the
+
+     VERNAC COMMAND EXTEND ... END
+
+   macros are not fully qualified.
+
+   This:
+
+     int(i)
+
+   means that the new command is expected to be followed by an integer.
+   The integer is bound in the parsing rule to variable i.
+   This variable i then can be used in the interpretation rule.
+
+   To see value of which Ocaml types can be bound this way,
+   look at the wit_* function declared in interp/stdarg.mli
+   (in the Coq's codebase).
+   
+   If we drop the wit_ prefix, we will get the token
+   that we can use in the parsing rule.
+   That is, since there exists wit_int, we know that
+   we can write:
+
+     int(i)
+
+   By looking at the signature of the wit_int function:
+
+     val wit_int : int uniform_genarg_type
+
+   we also know that variable i will have the type int.
+
+   The types of wit_* functions are either:
+
+     'c uniform_genarg_type
+
+   or
+
+     ('a,'b,'c) genarg_type
+
+   In both cases, the bound variable will have type 'c.
+*)
+
+(* -------------------------------------------------------------------------- *)
+(*                                                                            *)
+(* How to define a new Vernacular command with variable number of arguments?  *)
+(*                                                                            *)
+(* -------------------------------------------------------------------------- *)
+
+VERNAC COMMAND EXTEND Cmd4 CLASSIFIED AS QUERY
+| [ "Cmd4" int_list(l) ] -> { () }
+END
+
+(*
+   This:
+
+     int_list(l)
+
+   means that the new Vernacular command is expected to be followed
+   by a (whitespace separated) list of integers.
+   This list of integers is bound to the indicated l.
+   
+   In this case, as well as in the cases we point out below, instead of int
+   in int_list we could use any other supported type, e.g. ident, bool, ...
+   
+   To see which other Ocaml type constructors (in addition to list)
+   are supported, have a look at the parse_user_entry function defined
+   in grammar/q_util.mlp file.
+   
+   E.g.:
+   - ne_int_list(x) would represent a non-empty list of integers,
+   - int_list(x) would represent a list of integers,
+   - int_opt(x) would represent a value of type int option,
+   - ···
+*)
+
+(* -------------------------------------------------------------------------- *)
+(*                                                                            *)
+(* How to define a new Vernacular command that takes values of a custom type? *)
+(*                                                                            *)
+(* -------------------------------------------------------------------------- *)
+
+{
+
+open Ltac_plugin
+
+}
+
+(*
+   If we want to avoid a compilation failure
+
+     "no implementation available for Tacenv"
+
+   then we have to open the Ltac_plugin module.
+*)
+
+(*
+   Pp module must be opened because some of the macros that are part of the API
+   do not expand to fully qualified names.
+*)
+
+{
+
+type type_5 = Foo_5 | Bar_5
+
+}
+
+(*
+   We define a type of values that we want to pass to our Vernacular command.
+*)
+
+(*
+   By default, we are able to define new Vernacular commands that can take
+   parameters of some of the supported types. Which types are supported,
+   that was discussed earlier.
+
+   If we want to be able to define Vernacular command that takes parameters
+   of a type that is not supported by default, we must use the following macro:
+*)
+
+{
+
+open Pp
+
+}
+
+VERNAC ARGUMENT EXTEND custom5
+| [ "Foo_5" ] -> { Foo_5 }
+| [ "Bar_5" ] -> { Bar_5 }
+END
+
+(*
+   where:
+
+     custom5
+
+   indicates that, from now on, in our parsing rules we can write:
+
+     custom5(some_variable)
+
+   in those places where we expect user to provide an input
+   that can be parsed by the parsing rules above
+   (and interpreted by the interpretations rules above).
+*)
+
+(* Here: *)
+
+VERNAC COMMAND EXTEND Cmd5 CLASSIFIED AS QUERY
+| [ "Cmd5" custom5(x) ] -> { () }
+END
+
+(*
+   we define a new Vernacular command whose parameters, provided by the user,
+   can be mapped to values of type_5.
+*)
+
+(* -------------------------------------------------------------------------- *)
+(*                                                                            *)
+(*                     How to give a feedback to the user?                    *)
+(*                                                                            *)
+(* -------------------------------------------------------------------------- *)
+
+VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY
+| [ "Cmd6" ] -> { Feedback.msg_notice (Pp.str "Everything is awesome!") }
+END
+
+(*
+   The following functions:
+
+     - Feedback.msg_info    : Pp.t -> unit
+     - Feedback.msg_notice  : Pp.t -> unit
+     - Feedback.msg_warning : Pp.t -> unit
+     - Feedback.msg_error   : Pp.t -> unit
+     - Feedback.msg_debug   : Pp.t -> unit
+
+   enable us to give user a textual feedback.
+
+   Pp module enable us to represent and construct pretty-printing instructions.
+   The concepts defined and the services provided by the Pp module are in
+   various respects related to the concepts and services provided
+   by the Format module that is part of the Ocaml standard library.
+*)
+
+(* -------------------------------------------------------------------------- *)
+(*                                                                            *)
+(*    How to implement a Vernacular command with (undoable) side-effects?     *)
+(*                                                                            *)
+(* -------------------------------------------------------------------------- *)
+
+{
+
+open Summary.Local
+
+}
+
+(*
+   By opening Summary.Local module we shadow the original functions
+   that we traditionally use for implementing stateful behavior.
+
+     ref
+     !
+     :=
+
+   are now shadowed by their counterparts in Summary.Local. *)
+
+{
+
+let counter = ref ~name:"counter" 0
+
+}
+
+VERNAC COMMAND EXTEND Cmd7 CLASSIFIED AS SIDEFF
+| [ "Cmd7" ] -> { counter := succ !counter;
+                  Feedback.msg_notice (Pp.str "counter = " ++ Pp.str (string_of_int (!counter))) }
+END
+
+TACTIC EXTEND tactic1
+| [ "tactic1" ] -> { Proofview.tclUNIT () }
+END
+
+(* ---- *)
+
+{
+
+type custom = Foo_2 | Bar_2
+
+let pr_custom _ _ _ = function
+  | Foo_2 -> Pp.str "Foo_2"
+  | Bar_2 -> Pp.str "Bar_2"
+
+}
+
+ARGUMENT EXTEND custom2 PRINTED BY { pr_custom }
+| [ "Foo_2" ] -> { Foo_2 }
+| [ "Bar_2" ] -> { Bar_2 }
+END
+
+TACTIC EXTEND tactic2
+| [ "tactic2" custom2(x) ] -> { Proofview.tclUNIT () }
+END
diff --git a/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack b/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack
new file mode 100644
index 0000000000..4f0b8480b5
--- /dev/null
+++ b/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack
@@ -0,0 +1 @@
+Demo
diff --git a/doc/plugin_tutorial/tuto2/src/dune b/doc/plugin_tutorial/tuto2/src/dune
new file mode 100644
index 0000000000..f2bc405455
--- /dev/null
+++ b/doc/plugin_tutorial/tuto2/src/dune
@@ -0,0 +1,9 @@
+(library
+ (name tuto2_plugin)
+ (public_name coq.plugins.tutorial.p2)
+ (libraries coq.plugins.ltac))
+
+(rule
+ (targets demo.ml)
+ (deps (:pp-file demo.mlg) )
+ (action (run coqpp %{pp-file})))
diff --git a/doc/plugin_tutorial/tuto2/theories/Test.v b/doc/plugin_tutorial/tuto2/theories/Test.v
new file mode 100644
index 0000000000..38e83bfff1
--- /dev/null
+++ b/doc/plugin_tutorial/tuto2/theories/Test.v
@@ -0,0 +1,19 @@
+Declare ML Module "demo_plugin".
+
+Cmd1.
+Cmd2 With Some Terminal Parameters.
+Cmd3 42.
+Cmd4 100 200 300 400.
+Cmd5 Foo_5.
+Cmd5 Bar_5.
+Cmd6.
+Cmd7.
+Cmd7.
+Cmd7.
+
+Goal True.
+Proof.
+  tactic1.
+  tactic2 Foo_2.
+  tactic2 Bar_2.
+Abort.
diff --git a/doc/plugin_tutorial/tuto3/Makefile b/doc/plugin_tutorial/tuto3/Makefile
new file mode 100644
index 0000000000..e0e197650d
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/Makefile
@@ -0,0 +1,14 @@
+ifeq "$(COQBIN)" ""
+  COQBIN=$(dir $(shell which coqtop))/
+endif
+
+%: Makefile.coq
+
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+
+tests: all
+	@$(MAKE) -C tests -s clean
+	@$(MAKE) -C tests -s all
+
+-include Makefile.coq
diff --git a/doc/plugin_tutorial/tuto3/_CoqProject b/doc/plugin_tutorial/tuto3/_CoqProject
new file mode 100644
index 0000000000..e2a60a430f
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/_CoqProject
@@ -0,0 +1,12 @@
+-R theories Tuto3
+-I src
+
+theories/Data.v
+theories/Loader.v
+
+src/tuto_tactic.ml
+src/tuto_tactic.mli
+src/construction_game.ml
+src/construction_game.mli
+src/g_tuto3.mlg
+src/tuto3_plugin.mlpack
diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.ml b/doc/plugin_tutorial/tuto3/src/construction_game.ml
new file mode 100644
index 0000000000..22b02f6893
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/src/construction_game.ml
@@ -0,0 +1,184 @@
+open Pp
+
+let example_sort evd =
+(* creating a new sort requires that universes should be recorded
+  in the evd datastructure, so this datastructure also needs to be
+  passed around. *)
+  let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
+  let new_type = EConstr.mkSort s in
+  evd, new_type
+
+let c_one evd =
+(* In the general case, global references may refer to universe polymorphic
+   objects, and their universe has to be made afresh when creating an instance. *)
+  let gr_S =
+    Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
+(* the long name of "S" was found with the command "About S." *)
+  let gr_O =
+    Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
+  let evd, c_O = Evarutil.new_global evd gr_O in
+  let evd, c_S = Evarutil.new_global evd gr_S in
+(* Here is the construction of a new term by applying functions to argument. *)
+  evd, EConstr.mkApp (c_S, [| c_O |])
+
+let dangling_identity env evd =
+(* I call this a dangling identity, because it is not polymorph, but
+   the type on which it applies is left unspecified, as it is
+   represented by an existential variable.  The declaration for this
+   existential variable needs to be added in the evd datastructure. *)
+  let evd, type_type = example_sort evd in
+  let evd, arg_type = Evarutil.new_evar env evd type_type in
+(* Notice the use of a De Bruijn index for the inner occurrence of the
+  bound variable. *)
+  evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
+          EConstr.mkRel 1)
+
+let dangling_identity2 env evd =
+(* This example uses directly a function that produces an evar that
+  is meant to be a type. *)
+  let evd, (arg_type, type_type) =
+    Evarutil.new_type_evar env evd Evd.univ_rigid in
+  evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
+          EConstr.mkRel 1)
+
+let example_sort_app_lambda () =
+    let env = Global.env () in
+    let evd = Evd.from_env env in
+    let evd, c_v = c_one evd in
+(* dangling_identity and dangling_identity2 can be used interchangeably here *)
+    let evd, c_f = dangling_identity2 env evd in
+    let c_1 = EConstr.mkApp (c_f, [| c_v |]) in
+    let _ = Feedback.msg_notice
+       (Printer.pr_econstr_env env evd c_1) in
+    (* type verification happens here.  Type verification will update
+       existential variable information in the evd part. *)
+    let evd, the_type = Typing.type_of env evd c_1 in
+(* At display time, you will notice that the system knows about the
+  existential variable being instantiated to the "nat" type, even
+  though c_1 still contains the meta-variable. *)
+    Feedback.msg_notice
+      ((Printer.pr_econstr_env env evd c_1) ++
+       str " has type " ++
+       (Printer.pr_econstr_env env evd the_type))
+
+
+let c_S evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
+  Evarutil.new_global evd gr
+
+let c_O evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
+  Evarutil.new_global evd gr
+
+let c_E evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in
+  Evarutil.new_global evd gr
+
+let c_D evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in
+  Evarutil.new_global evd gr
+
+let c_Q evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in
+  Evarutil.new_global evd gr
+
+let c_R evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in
+  Evarutil.new_global evd gr
+
+let c_N evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in
+  Evarutil.new_global evd gr
+
+let c_C evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "C" in
+  Evarutil.new_global evd gr
+
+let c_F evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in
+  Evarutil.new_global evd gr
+
+let c_P evd =
+  let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in
+  Evarutil.new_global evd gr
+
+(* If c_S was universe polymorphic, we should have created a new constant
+   at each iteration of buildup. *)
+let mk_nat evd n =
+  let evd, c_S = c_S evd in
+  let evd, c_O = c_O evd in
+  let rec buildup = function
+    | 0 -> c_O
+    | n -> EConstr.mkApp (c_S, [| buildup (n - 1) |]) in
+  if n <= 0 then evd, c_O else evd, buildup n
+
+let example_classes n =
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let evd, c_n = mk_nat evd n in
+  let evd, n_half = mk_nat evd (n / 2) in
+  let evd, c_N = c_N evd in
+  let evd, c_div = c_D evd in
+  let evd, c_even = c_E evd in
+  let evd, c_Q = c_Q evd in
+  let evd, c_R = c_R evd in
+  let arg_type = EConstr.mkApp (c_even, [| c_n |]) in
+  let evd0 = evd in
+  let evd, instance = Evarutil.new_evar env evd arg_type in
+  let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in
+  let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in
+  let evd, the_type = Typing.type_of env evd c_half in
+  let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in
+  let proved_equality =
+    EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.DEFAULTcast,
+      EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in
+(* This is where we force the system to compute with type classes. *)
+(* Question to coq developers: why do we pass two evd arguments to
+   solve_remaining_evars? Is the choice of evd0 relevant here? *)
+  let evd = Pretyping.solve_remaining_evars
+    (Pretyping.default_inference_flags true) env evd ~initial:evd0 in
+  let evd, final_type = Typing.type_of env evd proved_equality in
+  Feedback.msg_notice (Printer.pr_econstr_env env evd proved_equality)
+
+(* This function, together with definitions in Data.v, shows how to
+   trigger automatic proofs at the time of typechecking, based on
+   canonical structures.
+
+   n is a number for which we want to find the half (and a proof that
+   this half is indeed the half)
+*)
+let example_canonical n =
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+(* Construct a natural representation of this integer. *)
+  let evd, c_n = mk_nat evd n in
+(* terms for "nat", "eq", "S_ev", "eq_refl", "C" *)
+  let evd, c_N = c_N evd in
+  let evd, c_F = c_F evd in
+  let evd, c_R = c_R evd in
+  let evd, c_C = c_C evd in
+  let evd, c_P = c_P evd in
+(* the last argument of C *)
+  let refl_term = EConstr.mkApp (c_R, [|c_N; c_n |]) in
+(* Now we build two existential variables, for the value of the half and for
+   the "S_ev" structure that triggers the proof search. *)
+  let evd, ev1 = Evarutil.new_evar env evd c_N in
+(* This is the type for the second existential variable *)
+  let csev = EConstr.mkApp (c_F, [| ev1 |]) in
+  let evd, ev2 = Evarutil.new_evar env evd csev in
+(* Now we build the C structure. *)
+  let test_term = EConstr.mkApp (c_C, [| c_n; ev1; ev2; refl_term |]) in
+(* Type-checking this term will compute values for the existential variables *)
+  let evd, final_type = Typing.type_of env evd test_term in
+(* The computed type has two parameters, the second one is the proof. *)
+  let value = match EConstr.kind evd final_type with
+      | Constr.App(_, [| _; the_half |]) -> the_half
+      | _ -> failwith "expecting the whole type to be \"cmp _ the_half\"" in
+  let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd value) in
+(* I wish for a nicer way to get the value of ev2 in the evar_map *)
+  let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in
+  let the_prf = EConstr.mkApp (c_P, [| ev1; prf_struct |]) in
+  let evd, the_statement = Typing.type_of env evd the_prf in
+  Feedback.msg_notice
+    (Printer.pr_econstr_env env evd the_prf ++ str " has type " ++
+     Printer.pr_econstr_env env evd the_statement)
diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.mli b/doc/plugin_tutorial/tuto3/src/construction_game.mli
new file mode 100644
index 0000000000..1832ed6630
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/src/construction_game.mli
@@ -0,0 +1,4 @@
+val dangling_identity : Environ.env -> Evd.evar_map -> Evd.evar_map * EConstr.t
+val example_sort_app_lambda : unit -> unit
+val example_classes : int -> unit
+val example_canonical : int -> unit
diff --git a/doc/plugin_tutorial/tuto3/src/dune b/doc/plugin_tutorial/tuto3/src/dune
new file mode 100644
index 0000000000..ba6d8b288f
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/src/dune
@@ -0,0 +1,10 @@
+(library
+ (name tuto3_plugin)
+ (public_name coq.plugins.tutorial.p3)
+ (flags :standard -warn-error -3)
+ (libraries coq.plugins.ltac))
+
+(rule
+ (targets g_tuto3.ml)
+ (deps (:pp-file g_tuto3.mlg))
+ (action (run coqpp %{pp-file})))
diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
new file mode 100644
index 0000000000..82ba45726e
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg
@@ -0,0 +1,46 @@
+DECLARE PLUGIN "tuto3_plugin"
+
+{
+
+open Ltac_plugin
+
+open Construction_game
+
+(* This one is necessary, to avoid message about missing wit_string *)
+open Stdarg
+
+}
+
+VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
+| [ "Tuto3_1" ] ->
+  { let env = Global.env () in
+    let evd = Evd.from_env env in
+    let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
+    let new_type_2 = EConstr.mkSort s in
+    let evd, _ =
+      Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in
+    Feedback.msg_notice
+      (Printer.pr_econstr_env env evd new_type_2) }
+END
+
+VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
+| [ "Tuto3_2" ] -> { example_sort_app_lambda () }
+END
+
+TACTIC EXTEND collapse_hyps
+| [ "pack" "hypothesis" ident(i) ] ->
+  { Tuto_tactic.pack_tactic i }
+END
+
+(* More advanced examples, where automatic proof happens but
+   no tactic is being called explicitely.  The first one uses
+   type classes. *)
+VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
+| [ "Tuto3_3" int(n) ] -> { example_classes n }
+END
+
+(* The second one uses canonical structures. *)
+VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY
+| [ "Tuto3_4" int(n) ] -> { example_canonical n }
+END
+
diff --git a/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack b/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack
new file mode 100644
index 0000000000..f4645ad7ed
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack
@@ -0,0 +1,3 @@
+Construction_game
+Tuto_tactic
+G_tuto3
diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
new file mode 100644
index 0000000000..9818867621
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
@@ -0,0 +1,143 @@
+open Proofview
+
+let constants = ref ([] : EConstr.t list)
+
+(* This is a pattern to collect terms from the Coq memory of valid terms
+  and proofs.  This pattern extends all the way to the definition of function
+ c_U *)
+let collect_constants () =
+  if (!constants = []) then
+    let open Coqlib in
+    let open EConstr in
+    let open UnivGen in
+    let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "pack" in
+    let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "packer" in
+    let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in
+    let gr_P = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "prod" in
+    let gr_U = find_reference "Tuto3" ["Tuto3"; "Data"] "uncover" in
+    constants := List.map (fun x -> of_constr (constr_of_monomorphic_global x))
+      [gr_H; gr_M; gr_R; gr_P; gr_U];
+    !constants
+  else
+    !constants
+
+let c_H () =
+  match collect_constants () with
+    it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of pack"
+
+let c_M () =
+  match collect_constants () with
+    _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of pack_marker"
+
+let c_R () =
+  match collect_constants () with
+    _ :: _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of pair"
+
+let c_P () =
+  match collect_constants () with
+    _ :: _ :: _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of prod"
+
+let c_U () =
+  match collect_constants () with
+    _ :: _ :: _ :: _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of prod"
+
+(* The following tactic is meant to pack an hypothesis when no other
+   data is already packed.
+
+   The main difficulty in defining this tactic is to understand how to
+   construct the input expected by apply_in. *)
+let package i = Goal.enter begin fun gl ->
+  Tactics.apply_in true false i
+   [(* this means that the applied theorem is not to be cleared. *)
+    None, (CAst.make (c_M (),
+           (* we don't specialize the theorem with extra values. *)
+           Tactypes.NoBindings))]
+     (* we don't destruct the result according to any intro_pattern *)
+    None
+  end
+
+(* This function is meant to observe a type of shape (f a)
+   and return the value a.  *)
+
+(* Remark by Maxime: look for destApp combinator. *)
+let unpack_type evd term =
+  let report () =
+    CErrors.user_err (Pp.str "expecting a packed type") in
+  match EConstr.kind evd term with
+  | Constr.App (_, [| ty |]) -> ty
+  | _ -> report ()
+
+(* This function is meant to observe a type of shape
+   A -> pack B -> C and return A, B, C
+  but it is not used in the current version of our tactic.
+  It is kept as an example. *)
+let two_lambda_pattern evd term =
+  let report () =
+    CErrors.user_err (Pp.str "expecting two nested implications") in
+(* Note that pattern-matching is always done through the EConstr.kind function,
+   which only provides one-level deep patterns. *)
+  match EConstr.kind evd term with
+  (* Here we recognize the outer implication *)
+  | Constr.Prod (_, ty1, l1) ->
+      (* Here we recognize the inner implication *)
+      (match EConstr.kind evd l1 with
+      | Constr.Prod (n2, packed_ty2, deep_conclusion) ->
+        (* Here we recognized that the second type is an application *)
+        ty1, unpack_type evd packed_ty2, deep_conclusion
+      | _ -> report ())
+  | _ -> report ()
+
+(* In the environment of the goal, we can get the type of an assumption
+  directly by a lookup.  The other solution is to call a low-cost retyping
+  function like *)
+let get_type_of_hyp env id =
+  match EConstr.lookup_named id env with
+  | Context.Named.Declaration.LocalAssum (_, ty) -> ty
+  | _ -> CErrors.user_err (let open Pp in
+                             str (Names.Id.to_string id) ++
+                             str " is not a plain hypothesis")
+
+let repackage i h_hyps_id = Goal.enter begin fun gl ->
+    let env = Goal.env gl in
+    let evd = Tacmach.New.project gl in
+    let concl = Tacmach.New.pf_concl gl in
+    let (ty1 : EConstr.t) = get_type_of_hyp env i in
+    let (packed_ty2 : EConstr.t) = get_type_of_hyp env h_hyps_id in
+    let ty2 = unpack_type evd packed_ty2 in
+    let new_packed_type = EConstr.mkApp (c_P (), [| ty1; ty2 |]) in
+    let open EConstr in
+    let new_packed_value =
+        mkApp (c_R (), [| ty1; ty2; mkVar i;
+          mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in
+    Refine.refine ~typecheck:true begin fun evd ->
+      let evd, new_goal = Evarutil.new_evar env evd
+          (mkProd (Names.Name.Anonymous,
+                     mkApp(c_H (), [| new_packed_type |]),
+                       Vars.lift 1 concl)) in
+        evd, mkApp (new_goal,
+                 [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |])
+      end
+    end
+
+let pack_tactic i =
+  let h_hyps_id = (Names.Id.of_string "packed_hyps") in
+  Proofview.Goal.enter begin fun gl ->
+    let hyps = Environ.named_context_val (Proofview.Goal.env gl) in
+    if not (Termops.mem_named_context_val i hyps) then
+      (CErrors.user_err
+          (Pp.str ("no hypothesis named" ^ (Names.Id.to_string i))))
+    else
+      if Termops.mem_named_context_val h_hyps_id hyps then
+          tclTHEN (repackage i h_hyps_id)
+            (tclTHEN (Tactics.clear [h_hyps_id; i])
+               (Tactics.introduction h_hyps_id))
+      else
+        tclTHEN (package i)
+          (tclTHEN (Tactics.rename_hyp [i, h_hyps_id])
+             (Tactics.move_hyp h_hyps_id Logic.MoveLast))
+    end
diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli b/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli
new file mode 100644
index 0000000000..dbf6cf48e2
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli
@@ -0,0 +1,3 @@
+val two_lambda_pattern :
+    Evd.evar_map -> EConstr.t -> EConstr.t * EConstr.t * EConstr.t
+val pack_tactic : Names.Id.t -> unit Proofview.tactic
diff --git a/doc/plugin_tutorial/tuto3/theories/Data.v b/doc/plugin_tutorial/tuto3/theories/Data.v
new file mode 100644
index 0000000000..0b07fee4f2
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/theories/Data.v
@@ -0,0 +1,68 @@
+Require Import ArithRing.
+
+Inductive pack (A: Type) : Type :=
+  packer : A -> pack A.
+
+Arguments packer {A}.
+
+Definition uncover (A : Type) (packed : pack A) : A :=
+  match packed with packer v => v end.
+
+Notation "!!!" := (pack _) (at level 0, only printing).
+
+(* The following data is used as material for automatic proofs
+  based on type classes. *)
+
+Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}.
+
+Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}.
+
+Lemma even_rec n h : 2 * h = n -> 2 * S h = S (S n).
+Proof. intros H; ring [H]. Qed.
+
+Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) :=
+ {half := S (@half _ p); half_prop := even_rec n (@half _ p) (@half_prop _ p)}.
+
+Definition tuto_div2 n (p : EvenNat n) := @half _ p.
+
+(* to be used in the following examples
+Compute (@half 8 _).
+
+Check (@half_prop 8 _).
+
+Check (@half_prop 7 _).
+
+and in command Tuto3_3 8. *)
+
+(* The following data is used as material for automatic proofs
+  based on canonical structures. *)
+
+Record S_ev n := Build_S_ev {double_of : nat; _ : 2 * n = double_of}.
+
+Definition s_half_proof n (r : S_ev n) : 2 * n = double_of n r :=
+  match r with Build_S_ev _ _ h => h end.
+
+Canonical Structure can_ev_default n d (Pd : 2 * n = d) : S_ev n :=
+  Build_S_ev n d Pd.
+
+Canonical Structure can_ev0 : S_ev 0 :=
+  Build_S_ev 0 0 (@eq_refl _ 0).
+
+Lemma can_ev_rec n : forall (s : S_ev n), S_ev (S n).
+Proof.
+intros s; exists (S (S (double_of _ s))).
+destruct s as [a P]. simpl. ring [P].
+Defined.
+
+Canonical Structure can_ev_rec.
+
+Record cmp (n : nat) (k : nat) :=
+  C {h : S_ev k; _ : double_of k h = n}.
+
+(* To be used in, e.g.,
+
+Check (C _ _ _ eq_refl : cmp 6 _).
+
+Check (C _ _ _ eq_refl : cmp 7 _).
+
+*)
diff --git a/doc/plugin_tutorial/tuto3/theories/Loader.v b/doc/plugin_tutorial/tuto3/theories/Loader.v
new file mode 100644
index 0000000000..1351cff63b
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/theories/Loader.v
@@ -0,0 +1,3 @@
+From Tuto3 Require Export Data.
+
+Declare ML Module "tuto3_plugin".
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.