Integrate build and documentation of Ltac2

Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.

Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.

86 files changed, 1094 insertions, 1774 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3c427793e2..fba68f633e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -172,9 +172,7 @@ after_script:
     - not-a-real-job
   script:
     - cd _install_ci
-    - find lib/coq/ -name '*.vo' -print0 > vofiles
-    - for regexp in 's/.vo//' 's:lib/coq/plugins:Coq:' 's:lib/coq/theories:Coq:' 's:/:.:g'; do sed -z -i "$regexp" vofiles; done
-    - xargs -0 --arg-file=vofiles bin/coqchk -silent -o -m -coqlib lib/coq/
+    - find lib/coq/ -name '*.vo' -print0 | xargs -0 bin/coqchk -silent -o -m -coqlib lib/coq/
 
 .ci-template:
   stage: test
diff --git a/Makefile b/Makefile
index 2b5d2cea16..c4404d13c7 100644
--- a/Makefile
+++ b/Makefile
@@ -66,7 +66,7 @@ FIND_SKIP_DIRS:='(' \
 ')' -prune -o
 
 define find
- $(shell find . $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||')
+ $(shell find . user-contrib/Ltac2 $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||')
 endef
 
 define findindir
diff --git a/Makefile.build b/Makefile.build
index 2a071fd820..034c9ea03c 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -158,11 +158,14 @@ endif
 VDFILE := .vfiles
 MLDFILE := .mlfiles
 PLUGMLDFILE := plugins/.mlfiles
+USERCONTRIBMLDFILE := user-contrib/.mlfiles
 MLLIBDFILE := .mllibfiles
 PLUGMLLIBDFILE := plugins/.mllibfiles
+USERCONTRIBMLLIBDFILE := user-contrib/.mllibfiles
 
 DEPENDENCIES := \
- $(addsuffix .d, $(MLDFILE) $(MLLIBDFILE) $(PLUGMLDFILE) $(PLUGMLLIBDFILE) $(CFILES) $(VDFILE))
+ $(addsuffix .d, $(MLDFILE) $(MLLIBDFILE) $(PLUGMLDFILE) $(PLUGMLLIBDFILE) \
+ $(USERCONTRIBMLDFILE) $(USERCONTRIBMLLIBDFILE) $(CFILES) $(VDFILE))
 
 -include $(DEPENDENCIES)
 
@@ -209,12 +212,14 @@ BOOTCOQC=$(TIMER) $(COQC) -coqlib . -q $(COQOPTS)
 LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS))
 MLINCLUDES=$(LOCALINCLUDES)
 
+USERCONTRIBINCLUDES=$(addprefix -I user-contrib/,$(USERCONTRIBDIRS))
+
 OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS)
 OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
 
 BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
 OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS)
-DEPFLAGS=$(LOCALINCLUDES) -map gramlib/.pack/gramlib.ml $(if $(filter plugins/%,$@),, -I ide -I ide/protocol)
+DEPFLAGS=$(LOCALINCLUDES) -map gramlib/.pack/gramlib.ml $(if $(filter plugins/% user-contrib/%,$@),, -I ide -I ide/protocol)
 
 # On MacOS, the binaries are signed, except our private ones
 ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin)
@@ -442,11 +447,11 @@ tools/coqdep_boot.cmx : tools/coqdep_common.cmx
 
 $(COQDEPBOOT): $(call bestobj, $(COQDEPBOOTSRC))
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, -I tools -package unix)
+	$(HIDE)$(call bestocaml, -I tools -package unix -package str)
 
 $(COQDEPBOOTBYTE): $(COQDEPBOOTSRC)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(call ocamlbyte, -I tools -package unix)
+	$(HIDE)$(call ocamlbyte, -I tools -package unix -package str)
 
 $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
@@ -567,7 +572,7 @@ VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -coqlib .
 
 validate: $(CHICKEN) | $(ALLVO:.$(VO)=.vo)
 	$(SHOW)'COQCHK <theories & plugins>'
-	$(HIDE)$(CHICKEN) $(VALIDOPTS) $(ALLMODS)
+	$(HIDE)$(CHICKEN) $(VALIDOPTS) $(ALLVO)
 
 $(ALLSTDLIB).v:
 	$(SHOW)'MAKE $(notdir $@)'
@@ -743,6 +748,10 @@ plugins/%.cmx: plugins/%.ml
 	$(SHOW)'OCAMLOPT  $<'
 	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $<
 
+user-contrib/%.cmx: user-contrib/%.ml
+	$(SHOW)'OCAMLOPT  $<'
+	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $<
+
 kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50
 
 %.cmx: %.ml
@@ -776,8 +785,8 @@ kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50
 # Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12)
 OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .mlpack
 
-MAINMLFILES := $(filter-out gramlib/.pack/% checker/% plugins/%, $(MLFILES) $(MLIFILES))
-MAINMLLIBFILES := $(filter-out gramlib/.pack/% checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES))
+MAINMLFILES := $(filter-out gramlib/.pack/% checker/% plugins/% user-contrib/%, $(MLFILES) $(MLIFILES))
+MAINMLLIBFILES := $(filter-out gramlib/.pack/% checker/% plugins/% user-contrib/%, $(MLLIBFILES) $(MLPACKFILES))
 
 $(MLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLFILES) $(D_DEPEND_AFTER_SRC) $(GENFILES) $(GENGRAMFILES)
 	$(SHOW)'OCAMLDEP  MLFILES MLIFILES'
@@ -796,6 +805,14 @@ $(PLUGMLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter plugins/%, $(MLLIBFILES) $(
 	$(SHOW)'OCAMLLIBDEP  plugins/MLLIBFILES plugins/MLPACKFILES'
 	$(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) $(filter plugins/%, $(MLLIBFILES) $(MLPACKFILES)) $(TOTARGET)
 
+$(USERCONTRIBMLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter user-contrib/%, $(MLFILES) $(MLIFILES)) $(D_DEPEND_AFTER_SRC) $(GENFILES)
+	$(SHOW)'OCAMLDEP  user-contrib/MLFILES user-contrib/MLIFILES'
+	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(filter user-contrib/%, $(MLFILES) $(MLIFILES)) $(TOTARGET)
+
+$(USERCONTRIBMLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter user-contrib/%, $(MLLIBFILES) $(MLPACKFILES)) $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES)
+	$(SHOW)'OCAMLLIBDEP  user-contrib/MLLIBFILES user-contrib/MLPACKFILES'
+	$(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) $(filter user-contrib/%, $(MLLIBFILES) $(MLPACKFILES)) $(TOTARGET)
+
 ###########################################################################
 # Compilation of .v files
 ###########################################################################
@@ -861,7 +878,7 @@ endif
 
 $(VDFILE).d: $(D_DEPEND_BEFORE_SRC) $(VFILES) $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT)
 	$(SHOW)'COQDEP    VFILES'
-	$(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) $(VFILES) $(TOTARGET)
+	$(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) -Q user-contrib "" $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET)
 
 ###########################################################################
 
diff --git a/Makefile.common b/Makefile.common
index bd0e19cd00..ee3bfb43c5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -104,10 +104,14 @@ PLUGINDIRS:=\
   rtauto 	nsatz           syntax          btauto \
   ssrmatching	ltac		ssr
 
+USERCONTRIBDIRS:=\
+	Ltac2
+
 SRCDIRS:=\
   $(CORESRCDIRS)  \
   tools 	tools/coqdoc	\
-  $(addprefix plugins/, $(PLUGINDIRS))
+  $(addprefix plugins/, $(PLUGINDIRS))  \
+  $(addprefix user-contrib/, $(USERCONTRIBDIRS))
 
 COQRUN := coqrun
 LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a
@@ -149,13 +153,14 @@ DERIVECMO:=plugins/derive/derive_plugin.cmo
 LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
 SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
+LTAC2CMO:=user-contrib/Ltac2/ltac2_plugin.cmo
 
 PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(MICROMEGACMO) \
         $(RINGCMO) \
         $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
         $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \
-	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO)
+	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) $(LTAC2CMO)
 
 ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
  STATICPLUGINS:=$(PLUGINSCMO)
diff --git a/Makefile.vofiles b/Makefile.vofiles
index a71d68e565..e05822c889 100644
--- a/Makefile.vofiles
+++ b/Makefile.vofiles
@@ -13,7 +13,7 @@ endif
 ###########################################################################
 
 THEORIESVO := $(patsubst %.v,%.$(VO),$(shell find theories -type f -name "*.v"))
-PLUGINSVO := $(patsubst %.v,%.$(VO),$(shell find plugins -type f -name "*.v"))
+PLUGINSVO := $(patsubst %.v,%.$(VO),$(shell find plugins user-contrib -type f -name "*.v"))
 ALLVO := $(THEORIESVO) $(PLUGINSVO)
 VFILES := $(ALLVO:.$(VO)=.v)
 
@@ -24,16 +24,16 @@ THEORIESLIGHTVO:= \
 
 # convert a (stdlib) filename into a module name:
 # remove .vo, replace theories and plugins by Coq, and replace slashes by dots
-vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
+vo_to_mod = $(subst /,.,$(patsubst user-contrib/%,%,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=)))))
 
 ALLMODS:=$(call vo_to_mod,$(ALLVO:.$(VO)=.vo))
 
 
 # Converting a stdlib filename into native compiler filenames
 # Used for install targets
-vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*)))))
+vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%, N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*))))))
 
-vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o)))))
+vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%, N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o))))))
 
 ifdef QUICK
 GLOBFILES:=
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index 0467852b19..85b02013d8 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -551,3 +551,20 @@ the Calculus of Inductive Constructions}},
   biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cpp/BoespflugDG11},
   bibsource = {dblp computer science bibliography, http://dblp.org}
 }
+
+@inproceedings{MilnerPrincipalTypeSchemes,
+ author = {Damas, Luis and Milner, Robin},
+ title = {Principal Type-schemes for Functional Programs},
+ booktitle = {Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+ series = {POPL '82},
+ year = {1982},
+ isbn = {0-89791-065-6},
+ location = {Albuquerque, New Mexico},
+ pages = {207--212},
+ numpages = {6},
+ url = {http://doi.acm.org/10.1145/582153.582176},
+ doi = {10.1145/582153.582176},
+ acmid = {582176},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}
diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst
index a91c6a9c5f..0a20d1c47b 100644
--- a/doc/sphinx/index.html.rst
+++ b/doc/sphinx/index.html.rst
@@ -42,6 +42,7 @@ Contents
    proof-engine/proof-handling
    proof-engine/tactics
    proof-engine/ltac
+   proof-engine/ltac2
    proof-engine/detailed-tactic-examples
    proof-engine/ssreflect-proof-language
 
diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst
index 708820fff7..5562736997 100644
--- a/doc/sphinx/index.latex.rst
+++ b/doc/sphinx/index.latex.rst
@@ -41,6 +41,7 @@ The proof engine
    proof-engine/proof-handling
    proof-engine/tactics
    proof-engine/ltac
+   proof-engine/ltac2
    proof-engine/detailed-tactic-examples
    proof-engine/ssreflect-proof-language
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 0322b43694..d3562b52c5 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1,7 +1,7 @@
 .. _ltac:
 
-The tactic language
-===================
+Ltac
+====
 
 This chapter gives a compact documentation of |Ltac|, the tactic language
 available in |Coq|. We start by giving the syntax, and next, we present the
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
new file mode 100644
index 0000000000..6e33862b39
--- /dev/null
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -0,0 +1,992 @@
+.. _ltac2:
+
+.. coqtop:: none
+
+   From Ltac2 Require Import Ltac2.
+
+Ltac2
+=====
+
+The Ltac tactic language is probably one of the ingredients of the success of
+Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac:
+
+- has often unclear semantics
+- is very non-uniform due to organic growth
+- lacks expressivity (data structures, combinators, types, ...)
+- is slow
+- is error-prone and fragile
+- has an intricate implementation
+
+Following the need of users that start developing huge projects relying
+critically on Ltac, we believe that we should offer a proper modern language
+that features at least the following:
+
+- at least informal, predictable semantics
+- a typing system
+- standard programming facilities (i.e. datatypes)
+
+This new language, called Ltac2, is described in this chapter. It is still
+experimental but we encourage nonetheless users to start testing it,
+especially wherever an advanced tactic language is needed. The previous
+implementation of Ltac, described in the previous chapter, will be referred to
+as Ltac1.
+
+.. _ltac2_design:
+
+General design
+--------------
+
+There are various alternatives to Ltac1, such that Mtac or Rtac for instance.
+While those alternatives can be quite distinct from Ltac1, we designed
+Ltac2 to be closest as reasonably possible to Ltac1, while fixing the
+aforementioned defects.
+
+In particular, Ltac2 is:
+
+- a member of the ML family of languages, i.e.
+
+  * a call-by-value functional language
+  * with effects
+  * together with Hindley-Milner type system
+
+- a language featuring meta-programming facilities for the manipulation of
+  Coq-side terms
+- a language featuring notation facilities to help writing palatable scripts
+
+We describe more in details each point in the remainder of this document.
+
+ML component
+------------
+
+Overview
+~~~~~~~~
+
+Ltac2 is a member of the ML family of languages, in the sense that it is an
+effectful call-by-value functional language, with static typing à la
+Hindley-Milner (see :cite:`MilnerPrincipalTypeSchemes`). It is commonly accepted
+that ML constitutes a sweet spot in PL design, as it is relatively expressive
+while not being either too lax (unlike dynamic typing) nor too strict
+(unlike, say, dependent types).
+
+The main goal of Ltac2 is to serve as a meta-language for Coq. As such, it
+naturally fits in the ML lineage, just as the historical ML was designed as
+the tactic language for the LCF prover. It can also be seen as a general-purpose
+language, by simply forgetting about the Coq-specific features.
+
+Sticking to a standard ML type system can be considered somewhat weak for a
+meta-language designed to manipulate Coq terms. In particular, there is no
+way to statically guarantee that a Coq term resulting from an Ltac2
+computation will be well-typed. This is actually a design choice, motivated
+by retro-compatibility with Ltac1. Instead, well-typedness is deferred to
+dynamic checks, allowing many primitive functions to fail whenever they are
+provided with an ill-typed term.
+
+The language is naturally effectful as it manipulates the global state of the
+proof engine. This allows to think of proof-modifying primitives as effects
+in a straightforward way. Semantically, proof manipulation lives in a monad,
+which allows to ensure that Ltac2 satisfies the same equations as a generic ML
+with unspecified effects would do, e.g. function reduction is substitution
+by a value.
+
+Type Syntax
+~~~~~~~~~~~
+
+At the level of terms, we simply elaborate on Ltac1 syntax, which is quite
+close to e.g. the one of OCaml. Types follow the simply-typed syntax of OCaml.
+
+The non-terminal :production:`lident` designates identifiers starting with a
+lowercase.
+
+.. productionlist:: coq
+   ltac2_type             : ( `ltac2_type`, ... , `ltac2_type` ) `ltac2_typeconst`
+                    : ( `ltac2_type` * ... * `ltac2_type` )
+                    : `ltac2_type` -> `ltac2_type`
+                    : `ltac2_typevar`
+   ltac2_typeconst        : ( `modpath` . )* `lident`
+   ltac2_typevar          : '`lident`
+   ltac2_typeparams       : ( `ltac2_typevar`, ... , `ltac2_typevar` )
+
+The set of base types can be extended thanks to the usual ML type
+declarations such as algebraic datatypes and records.
+
+Built-in types include:
+
+- ``int``, machine integers (size not specified, in practice inherited from OCaml)
+- ``string``, mutable strings
+- ``'a array``, mutable arrays
+- ``exn``, exceptions
+- ``constr``, kernel-side terms
+- ``pattern``, term patterns
+- ``ident``, well-formed identifiers
+
+Type declarations
+~~~~~~~~~~~~~~~~~
+
+One can define new types by the following commands.
+
+.. cmd:: Ltac2 Type @ltac2_typeparams @lident
+   :name: Ltac2 Type
+
+   This command defines an abstract type. It has no use for the end user and
+   is dedicated to types representing data coming from the OCaml world.
+
+.. cmdv:: Ltac2 Type {? rec} @ltac2_typeparams @lident := @ltac2_typedef
+
+   This command defines a type with a manifest. There are four possible
+   kinds of such definitions: alias, variant, record and open variant types.
+
+   .. productionlist:: coq
+      ltac2_typedef    : `ltac2_type`
+                       : [ `ltac2_constructordef` | ... | `ltac2_constructordef` ]
+                       : { `ltac2_fielddef` ; ... ; `ltac2_fielddef` }
+                       : [ .. ]
+      ltac2_constructordef   : `uident` [ ( `ltac2_type` , ... , `ltac2_type` ) ]
+      ltac2_fielddef         : [ mutable ] `ident` : `ltac2_type`
+
+   Aliases are just a name for a given type expression and are transparently
+   unfoldable to it. They cannot be recursive. The non-terminal
+   :production:`uident` designates identifiers starting with an uppercase.
+
+   Variants are sum types defined by constructors and eliminated by
+   pattern-matching. They can be recursive, but the `rec` flag must be
+   explicitly set. Pattern-maching must be exhaustive.
+
+   Records are product types with named fields and eliminated by projection.
+   Likewise they can be recursive if the `rec` flag is set.
+
+   .. cmdv:: Ltac2 Type @ltac2_typeparams @ltac2_qualid := [ @ltac2_constructordef ]
+
+      Open variants are a special kind of variant types whose constructors are not
+      statically defined, but can instead be extended dynamically. A typical example
+      is the standard `exn` type. Pattern-matching must always include a catch-all
+      clause. They can be extended by this command.
+
+Term Syntax
+~~~~~~~~~~~
+
+The syntax of the functional fragment is very close to the one of Ltac1, except
+that it adds a true pattern-matching feature, as well as a few standard
+constructions from ML.
+
+.. productionlist:: coq
+   ltac2_var        : `lident`
+   ltac2_qualid     : ( `modpath` . )* `lident`
+   ltac2_constructor: `uident`
+   ltac2_term       : `ltac2_qualid`
+                    : `ltac2_constructor`
+                    : `ltac2_term` `ltac2_term` ... `ltac2_term`
+                    : fun `ltac2_var` => `ltac2_term`
+                    : let `ltac2_var` := `ltac2_term` in `ltac2_term`
+                    : let rec `ltac2_var` := `ltac2_term` in `ltac2_term`
+                    : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end
+                    : `int`
+                    : `string`
+                    : `ltac2_term` ; `ltac2_term`
+                    : [| `ltac2_term` ; ... ; `ltac2_term` |]
+                    : ( `ltac2_term` , ... , `ltac2_term` )
+                    : { `ltac2_field` `ltac2_field` ... `ltac2_field` }
+                    : `ltac2_term` . ( `ltac2_qualid` )
+                    : `ltac2_term` . ( `ltac2_qualid` ) := `ltac2_term`
+                    : [; `ltac2_term` ; ... ; `ltac2_term` ]
+                    : `ltac2_term` :: `ltac2_term`
+                    : ...
+   ltac2_branch     : `ltac2_pattern` => `ltac2_term`
+   ltac2_pattern    : `ltac2_var`
+                    : _
+                    : ( `ltac2_pattern` , ... , `ltac2_pattern` )
+                    : `ltac2_constructor` `ltac2_pattern` ... `ltac2_pattern`
+                    : [ ]
+                    : `ltac2_pattern` :: `ltac2_pattern`
+   ltac2_field      : `ltac2_qualid` := `ltac2_term`
+
+In practice, there is some additional syntactic sugar that allows e.g. to
+bind a variable and match on it at the same time, in the usual ML style.
+
+There is a dedicated syntax for list and array literals.
+
+.. note::
+
+   For now, deep pattern matching is not implemented.
+
+Ltac Definitions
+~~~~~~~~~~~~~~~~
+
+.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_term
+   :name: Ltac2
+
+   This command defines a new global Ltac2 value.
+
+   For semantic reasons, the body of the Ltac2 definition must be a syntactical
+   value, i.e. a function, a constant or a pure constructor recursively applied to
+   values.
+
+   If ``rec`` is set, the tactic is expanded into a recursive binding.
+
+   If ``mutable`` is set, the definition can be redefined at a later stage (see below).
+
+.. cmd:: Ltac2 Set @qualid := @ltac2_term
+   :name: Ltac2 Set
+
+   This command redefines a previous ``mutable`` definition.
+   Mutable definitions act like dynamic binding, i.e. at runtime, the last defined
+   value for this entry is chosen. This is useful for global flags and the like.
+
+Reduction
+~~~~~~~~~
+
+We use the usual ML call-by-value reduction, with an otherwise unspecified
+evaluation order. This is a design choice making it compatible with OCaml,
+if ever we implement native compilation. The expected equations are as follows::
+
+  (fun x => t) V ≡ t{x := V} (βv)
+
+  let x := V in t ≡ t{x := V} (let)
+
+  match C V₀ ... Vₙ with ... | C x₀ ... xₙ  => t | ... end ≡ t {xᵢ := Vᵢ} (ι)
+
+  (t any term, V values, C constructor)
+
+Note that call-by-value reduction is already a departure from Ltac1 which uses
+heuristics to decide when evaluating an expression. For instance, the following
+expressions do not evaluate the same way in Ltac1.
+
+:n:`foo (idtac; let x := 0 in bar)`
+
+:n:`foo (let x := 0 in bar)`
+
+Instead of relying on the :n:`idtac` idiom, we would now require an explicit thunk
+not to compute the argument, and :n:`foo` would have e.g. type
+:n:`(unit -> unit) -> unit`.
+
+:n:`foo (fun () => let x := 0 in bar)`
+
+Typing
+~~~~~~
+
+Typing is strict and follows Hindley-Milner system. Unlike Ltac1, there
+are no type casts at runtime, and one has to resort to conversion
+functions. See notations though to make things more palatable.
+
+In this setting, all usual argument-free tactics have type :n:`unit -> unit`, but
+one can return as well a value of type :n:`t` thanks to terms of type :n:`unit -> t`,
+or take additional arguments.
+
+Effects
+~~~~~~~
+
+Effects in Ltac2 are straightforward, except that instead of using the
+standard IO monad as the ambient effectful world, Ltac2 is going to use the
+tactic monad.
+
+Note that the order of evaluation of application is *not* specified and is
+implementation-dependent, as in OCaml.
+
+We recall that the `Proofview.tactic` monad is essentially a IO monad together
+with backtracking state representing the proof state.
+
+Intuitively a thunk of type :n:`unit -> 'a` can do the following:
+
+- It can perform non-backtracking IO like printing and setting mutable variables
+- It can fail in a non-recoverable way
+- It can use first-class backtrack. The proper way to figure that is that we
+  morally have the following isomorphism:
+  :n:`(unit -> 'a) ~ (unit -> exn + ('a * (exn -> 'a)))`
+  i.e. thunks can produce a lazy list of results where each
+  tail is waiting for a continuation exception.
+- It can access a backtracking proof state, made out amongst other things of
+  the current evar assignation and the list of goals under focus.
+
+We describe more thoroughly the various effects existing in Ltac2 hereafter.
+
+Standard IO
++++++++++++
+
+The Ltac2 language features non-backtracking IO, notably mutable data and
+printing operations.
+
+Mutable fields of records can be modified using the set syntax. Likewise,
+built-in types like `string` and `array` feature imperative assignment. See
+modules `String` and `Array` respectively.
+
+A few printing primitives are provided in the `Message` module, allowing to
+display information to the user.
+
+Fatal errors
+++++++++++++
+
+The Ltac2 language provides non-backtracking exceptions, also known as *panics*,
+through the following primitive in module `Control`.::
+
+  val throw : exn -> 'a
+
+Unlike backtracking exceptions from the next section, this kind of error
+is never caught by backtracking primitives, that is, throwing an exception
+destroys the stack. This is materialized by the following equation, where `E`
+is an evaluation context.::
+
+  E[throw e] ≡ throw e
+
+  (e value)
+
+There is currently no way to catch such an exception and it is a design choice.
+There might be at some future point a way to catch it in a brutal way,
+destroying all backtrack and return values.
+
+Backtrack
++++++++++
+
+In Ltac2, we have the following backtracking primitives, defined in the
+`Control` module.::
+
+  Ltac2 Type 'a result := [ Val ('a) | Err (exn) ].
+
+  val zero : exn -> 'a
+  val plus : (unit -> 'a) -> (exn -> 'a) -> 'a
+  val case : (unit -> 'a) -> ('a * (exn -> 'a)) result
+
+If one sees thunks as lazy lists, then `zero` is the empty list and `plus` is
+list concatenation, while `case` is pattern-matching.
+
+The backtracking is first-class, i.e. one can write
+:n:`plus (fun () => "x") (fun _ => "y") : string` producing a backtracking string.
+
+These operations are expected to satisfy a few equations, most notably that they
+form a monoid compatible with sequentialization.::
+
+  plus t zero ≡ t ()
+  plus (fun () => zero e) f ≡ f e
+  plus (plus t f) g ≡ plus t (fun e => plus (f e) g)
+
+  case (fun () => zero e) ≡ Err e
+  case (fun () => plus (fun () => t) f) ≡ Val (t,f)
+
+  let x := zero e in u ≡ zero e
+  let x := plus t f in u ≡ plus (fun () => let x := t in u) (fun e => let x := f e in u)
+
+  (t, u, f, g, e values)
+
+Goals
++++++
+
+A goal is given by the data of its conclusion and hypotheses, i.e. it can be
+represented as `[Γ ⊢ A]`.
+
+The tactic monad naturally operates over the whole proofview, which may
+represent several goals, including none. Thus, there is no such thing as
+*the current goal*. Goals are naturally ordered, though.
+
+It is natural to do the same in Ltac2, but we must provide a way to get access
+to a given goal. This is the role of the `enter` primitive, that applies a
+tactic to each currently focused goal in turn.::
+
+  val enter : (unit -> unit) -> unit
+
+It is guaranteed that when evaluating `enter f`, `f` is called with exactly one
+goal under focus. Note that `f` may be called several times, or never, depending
+on the number of goals under focus before the call to `enter`.
+
+Accessing the goal data is then implicit in the Ltac2 primitives, and may panic
+if the invariants are not respected. The two essential functions for observing
+goals are given below.::
+
+  val hyp : ident -> constr
+  val goal : unit -> constr
+
+The two above functions panic if there is not exactly one goal under focus.
+In addition, `hyp` may also fail if there is no hypothesis with the
+corresponding name.
+
+Meta-programming
+----------------
+
+Overview
+~~~~~~~~
+
+One of the major implementation issues of Ltac1 is the fact that it is
+never clear whether an object refers to the object world or the meta-world.
+This is an incredible source of slowness, as the interpretation must be
+aware of bound variables and must use heuristics to decide whether a variable
+is a proper one or referring to something in the Ltac context.
+
+Likewise, in Ltac1, constr parsing is implicit, so that ``foo 0`` is
+not ``foo`` applied to the Ltac integer expression ``0`` (Ltac does have a
+notion of integers, though it is not first-class), but rather the Coq term
+:g:`Datatypes.O`.
+
+The implicit parsing is confusing to users and often gives unexpected results.
+Ltac2 makes these explicit using quoting and unquoting notation, although there
+are notations to do it in a short and elegant way so as not to be too cumbersome
+to the user.
+
+Generic Syntax for Quotations
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+In general, quotations can be introduced in terms using the following syntax, where
+:production:`quotentry` is some parsing entry.
+
+.. prodn::
+   ltac2_term += @ident : ( @quotentry )
+
+Built-in quotations
++++++++++++++++++++
+
+The current implementation recognizes the following built-in quotations:
+
+- ``ident``, which parses identifiers (type ``Init.ident``).
+- ``constr``, which parses Coq terms and produces an-evar free term at runtime
+  (type ``Init.constr``).
+- ``open_constr``, which parses Coq terms and produces a term potentially with
+  holes at runtime (type ``Init.constr`` as well).
+- ``pattern``, which parses Coq patterns and produces a pattern used for term
+  matching (type ``Init.pattern``).
+- ``reference``, which parses either a :n:`@qualid` or :n:`& @ident`. Qualified names
+  are globalized at internalization into the corresponding global reference,
+  while ``&id`` is turned into ``Std.VarRef id``. This produces at runtime a
+  ``Std.reference``.
+
+The following syntactic sugar is provided for two common cases.
+
+- ``@id`` is the same as ``ident:(id)``
+- ``'t`` is the same as ``open_constr:(t)``
+
+Strict vs. non-strict mode
+++++++++++++++++++++++++++
+
+Depending on the context, quotations producing terms (i.e. ``constr`` or
+``open_constr``) are not internalized in the same way. There are two possible
+modes, respectively called the *strict* and the *non-strict* mode.
+
+- In strict mode, all simple identifiers appearing in a term quotation are
+  required to be resolvable statically. That is, they must be the short name of
+  a declaration which is defined globally, excluding section variables and
+  hypotheses. If this doesn't hold, internalization will fail. To work around
+  this error, one has to specifically use the ``&`` notation.
+- In non-strict mode, any simple identifier appearing in a term quotation which
+  is not bound in the global context is turned into a dynamic reference to a
+  hypothesis. That is to say, internalization will succeed, but the evaluation
+  of the term at runtime will fail if there is no such variable in the dynamic
+  context.
+
+Strict mode is enforced by default, e.g. for all Ltac2 definitions. Non-strict
+mode is only set when evaluating Ltac2 snippets in interactive proof mode. The
+rationale is that it is cumbersome to explicitly add ``&`` interactively, while it
+is expected that global tactics enforce more invariants on their code.
+
+Term Antiquotations
+~~~~~~~~~~~~~~~~~~~
+
+Syntax
+++++++
+
+One can also insert Ltac2 code into Coq terms, similarly to what is possible in
+Ltac1.
+
+.. prodn::
+   term += ltac2:( @ltac2_term )
+
+Antiquoted terms are expected to have type ``unit``, as they are only evaluated
+for their side-effects.
+
+Semantics
++++++++++
+
+Interpretation of a quoted Coq term is done in two phases, internalization and
+evaluation.
+
+- Internalization is part of the static semantics, i.e. it is done at Ltac2
+  typing time.
+- Evaluation is part of the dynamic semantics, i.e. it is done when
+  a term gets effectively computed by Ltac2.
+
+Note that typing of Coq terms is a *dynamic* process occurring at Ltac2
+evaluation time, and not at Ltac2 typing time.
+
+Static semantics
+****************
+
+During internalization, Coq variables are resolved and antiquotations are
+type-checked as Ltac2 terms, effectively producing a ``glob_constr`` in Coq
+implementation terminology. Note that although it went through the
+type-checking of **Ltac2**, the resulting term has not been fully computed and
+is potentially ill-typed as a runtime **Coq** term.
+
+.. example::
+
+   The following term is valid (with type `unit -> constr`), but will fail at runtime:
+
+   .. coqtop:: in
+
+      Ltac2 myconstr () := constr:(nat -> 0).
+
+Term antiquotations are type-checked in the enclosing Ltac2 typing context
+of the corresponding term expression.
+
+.. example::
+
+   The following will type-check, with type `constr`.
+
+   .. coqdoc::
+
+      let x := '0 in constr:(1 + ltac2:(exact x))
+
+Beware that the typing environment of antiquotations is **not**
+expanded by the Coq binders from the term.
+
+  .. example::
+
+     The following Ltac2 expression will **not** type-check::
+
+     `constr:(fun x : nat => ltac2:(exact x))`
+     `(* Error: Unbound variable 'x' *)`
+
+There is a simple reason for that, which is that the following expression would
+not make sense in general.
+
+`constr:(fun x : nat => ltac2:(clear @x; exact x))`
+
+Indeed, a hypothesis can suddenly disappear from the runtime context if some
+other tactic pulls the rug from under you.
+
+Rather, the tactic writer has to resort to the **dynamic** goal environment,
+and must write instead explicitly that she is accessing a hypothesis, typically
+as follows.
+
+`constr:(fun x : nat => ltac2:(exact (hyp @x)))`
+
+This pattern is so common that we provide dedicated Ltac2 and Coq term notations
+for it.
+
+- `&x` as an Ltac2 expression expands to `hyp @x`.
+- `&x` as a Coq constr expression expands to
+  `ltac2:(Control.refine (fun () => hyp @x))`.
+
+Dynamic semantics
+*****************
+
+During evaluation, a quoted term is fully evaluated to a kernel term, and is
+in particular type-checked in the current environment.
+
+Evaluation of a quoted term goes as follows.
+
+- The quoted term is first evaluated by the pretyper.
+- Antiquotations are then evaluated in a context where there is exactly one goal
+  under focus, with the hypotheses coming from the current environment extended
+  with the bound variables of the term, and the resulting term is fed into the
+  quoted term.
+
+Relative orders of evaluation of antiquotations and quoted term are not
+specified.
+
+For instance, in the following example, `tac` will be evaluated in a context
+with exactly one goal under focus, whose last hypothesis is `H : nat`. The
+whole expression will thus evaluate to the term :g:`fun H : nat => H`.
+
+`let tac () := hyp @H in constr:(fun H : nat => ltac2:(tac ()))`
+
+Many standard tactics perform type-checking of their argument before going
+further. It is your duty to ensure that terms are well-typed when calling
+such tactics. Failure to do so will result in non-recoverable exceptions.
+
+**Trivial Term Antiquotations**
+
+It is possible to refer to a variable of type `constr` in the Ltac2 environment
+through a specific syntax consistent with the antiquotations presented in
+the notation section.
+
+.. prodn:: term += $@lident
+
+In a Coq term, writing :g:`$x` is semantically equivalent to
+:g:`ltac2:(Control.refine (fun () => x))`, up to re-typechecking. It allows to
+insert in a concise way an Ltac2 variable of type :n:`constr` into a Coq term.
+
+Match over terms
+~~~~~~~~~~~~~~~~
+
+Ltac2 features a construction similar to Ltac1 :n:`match` over terms, although
+in a less hard-wired way.
+
+.. productionlist:: coq
+   ltac2_term       : match! `ltac2_term` with `constrmatching` .. `constrmatching` end
+                    : lazy_match! `ltac2_term` with `constrmatching` .. `constrmatching` end
+                    : multi_match! `ltac2_term` with `constrmatching` .. `constrmatching` end
+   constrmatching  : | `constrpattern` => `ltac2_term`
+   constrpattern   : `term`
+                   : context  [ `term` ]
+                   : context `lident` [ `term` ]
+
+This construction is not primitive and is desugared at parsing time into
+calls to term matching functions from the `Pattern` module. Internally, it is
+implemented thanks to a specific scope accepting the :n:`@constrmatching` syntax.
+
+Variables from the :n:`@constrpattern` are statically bound in the body of the branch, to
+values of type `constr` for the variables from the :n:`@constr` pattern and to a
+value of type `Pattern.context` for the variable :n:`@lident`.
+
+Note that unlike Ltac, only lowercase identifiers are valid as Ltac2
+bindings, so that there will be a syntax error if one of the bound variables
+starts with an uppercase character.
+
+The semantics of this construction is otherwise the same as the corresponding
+one from Ltac1, except that it requires the goal to be focused.
+
+Match over goals
+~~~~~~~~~~~~~~~~
+
+Similarly, there is a way to match over goals in an elegant way, which is
+just a notation desugared at parsing time.
+
+.. productionlist:: coq
+   ltac2_term             : match! [ reverse ] goal with `goalmatching` ... `goalmatching` end
+                    : lazy_match! [ reverse ] goal with `goalmatching` ... `goalmatching` end
+                    : multi_match! [ reverse ] goal with `goalmatching` ... `goalmatching` end
+   goalmatching     : | [ `hypmatching` ... `hypmatching` |- `constrpattern` ] => `ltac2_term`
+   hypmatching      : `lident` : `constrpattern`
+                    : _ : `constrpattern`
+
+Variables from :n:`@hypmatching` and :n:`@constrpattern` are bound in the body of the
+branch. Their types are:
+
+- ``constr`` for pattern variables appearing in a :n:`@term`
+- ``Pattern.context`` for variables binding a context
+- ``ident`` for variables binding a hypothesis name.
+
+The same identifier caveat as in the case of matching over constr applies, and
+this features has the same semantics as in Ltac1. In particular, a ``reverse``
+flag can be specified to match hypotheses from the more recently introduced to
+the least recently introduced one.
+
+Notations
+---------
+
+Notations are the crux of the usability of Ltac1. We should be able to recover
+a feeling similar to the old implementation by using and abusing notations.
+
+Scopes
+~~~~~~
+
+A scope is a name given to a grammar entry used to produce some Ltac2 expression
+at parsing time. Scopes are described using a form of S-expression.
+
+.. prodn::
+   ltac2_scope ::= @string %| @integer %| @lident ({+, @ltac2_scope})
+
+A few scopes contain antiquotation features. For sake of uniformity, all
+antiquotations are introduced by the syntax :n:`$@lident`.
+
+The following scopes are built-in.
+
+- :n:`constr`:
+
+  + parses :n:`c = @term` and produces :n:`constr:(c)`
+
+- :n:`ident`:
+
+  + parses :n:`id = @ident` and produces :n:`ident:(id)`
+  + parses :n:`$(x = @ident)` and produces the variable :n:`x`
+
+- :n:`list0(@ltac2_scope)`:
+
+  + if :n:`@ltac2_scope` parses :production:`entry`, parses :n:`(@entry__0, ..., @entry__n)` and produces
+    :n:`[@entry__0; ...; @entry__n]`.
+
+- :n:`list0(@ltac2_scope, sep = @string__sep)`:
+
+  + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`(@entry__0 @string__sep ... @string__sep @entry__n)`
+    and produces :n:`[@entry__0; ...; @entry__n]`.
+
+- :n:`list1`: same as :n:`list0` (with or without separator) but parses :n:`{+ @entry}` instead
+  of :n:`{* @entry}`.
+
+- :n:`opt(@ltac2_scope)`
+
+  + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`{? @entry}` and produces either :n:`None` or
+    :n:`Some x` where :n:`x` is the parsed expression.
+
+- :n:`self`:
+
+  + parses a Ltac2 expression at the current level and return it as is.
+
+- :n:`next`:
+
+  + parses a Ltac2 expression at the next level and return it as is.
+
+- :n:`tactic(n = @integer)`:
+
+  + parses a Ltac2 expression at the provided level :n:`n` and return it as is.
+
+- :n:`thunk(@ltac2_scope)`:
+
+  + parses the same as :n:`scope`, and if :n:`e` is the parsed expression, returns
+    :n:`fun () => e`.
+
+- :n:`STRING`:
+
+  + parses the corresponding string as an identifier and returns :n:`()`.
+
+- :n:`keyword(s = @string)`:
+
+  + parses the string :n:`s` as a keyword and returns `()`.
+
+- :n:`terminal(s = @string)`:
+
+  + parses the string :n:`s` as a keyword, if it is already a
+    keyword, otherwise as an :n:`@ident`. Returns `()`.
+
+- :n:`seq(@ltac2_scope__1, ..., @ltac2_scope__2)`:
+
+  + parses :n:`scope__1`, ..., :n:`scope__n` in this order, and produces a tuple made
+    out of the parsed values in the same order. As an optimization, all
+    subscopes of the form :n:`STRING` are left out of the returned tuple, instead
+    of returning a useless unit value. It is forbidden for the various
+    subscopes to refer to the global entry using self or next.
+
+A few other specific scopes exist to handle Ltac1-like syntax, but their use is
+discouraged and they are thus not documented.
+
+For now there is no way to declare new scopes from Ltac2 side, but this is
+planned.
+
+Notations
+~~~~~~~~~
+
+The Ltac2 parser can be extended by syntactic notations.
+
+.. cmd:: Ltac2 Notation {+ @lident (@ltac2_scope) %| @string } {? : @integer} := @ltac2_term
+   :name: Ltac2 Notation
+
+   A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded
+   to the provided body where every token from the notation is let-bound to the
+   corresponding generated expression.
+
+   .. example::
+
+      Assume we perform:
+
+      .. coqdoc::
+
+         Ltac2 Notation "foo" c(thunk(constr)) ids(list0(ident)) := Bar.f c ids.
+
+      Then the following expression
+
+      `let y := @X in foo (nat -> nat) x $y`
+
+      will expand at parsing time to
+
+      `let y := @X in`
+      `let c := fun () => constr:(nat -> nat) with ids := [@x; y] in Bar.f c ids`
+
+      Beware that the order of evaluation of multiple let-bindings is not specified,
+      so that you may have to resort to thunking to ensure that side-effects are
+      performed at the right time.
+
+Abbreviations
+~~~~~~~~~~~~~
+
+.. cmdv:: Ltac2 Notation @lident := @ltac2_term
+
+  This command introduces a special kind of notations, called abbreviations,
+  that is designed so that it does not add any parsing rules. It is similar in
+  spirit to Coq abbreviations, insofar as its main purpose is to give an
+  absolute name to a piece of pure syntax, which can be transparently referred
+  by this name as if it were a proper definition.
+
+  The abbreviation can then be manipulated just as a normal Ltac2 definition,
+  except that it is expanded at internalization time into the given expression.
+  Furthermore, in order to make this kind of construction useful in practice in
+  an effectful language such as Ltac2, any syntactic argument to an abbreviation
+  is thunked on-the-fly during its expansion.
+
+For instance, suppose that we define the following.
+
+:n:`Ltac2 Notation foo := fun x => x ().`
+
+Then we have the following expansion at internalization time.
+
+:n:`foo 0 ↦ (fun x => x ()) (fun _ => 0)`
+
+Note that abbreviations are not typechecked at all, and may result in typing
+errors after expansion.
+
+Evaluation
+----------
+
+Ltac2 features a toplevel loop that can be used to evaluate expressions.
+
+.. cmd:: Ltac2 Eval @ltac2_term
+   :name: Ltac2 Eval
+
+   This command evaluates the term in the current proof if there is one, or in the
+   global environment otherwise, and displays the resulting value to the user
+   together with its type. This command is pure in the sense that it does not
+   modify the state of the proof, and in particular all side-effects are discarded.
+
+Debug
+-----
+
+.. opt:: Ltac2 Backtrace
+
+   When this option is set, toplevel failures will be printed with a backtrace.
+
+Compatibility layer with Ltac1
+------------------------------
+
+Ltac1 from Ltac2
+~~~~~~~~~~~~~~~~
+
+Simple API
+++++++++++
+
+One can call Ltac1 code from Ltac2 by using the :n:`ltac1` quotation. It parses
+a Ltac1 expression, and semantics of this quotation is the evaluation of the
+corresponding code for its side effects. In particular, it cannot return values,
+and the quotation has type :n:`unit`.
+
+Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited
+to the use of standalone function calls.
+
+Low-level API
++++++++++++++
+
+There exists a lower-level FFI into Ltac1 that is not recommended for daily use,
+which is available in the `Ltac2.Ltac1` module. This API allows to directly
+manipulate dynamically-typed Ltac1 values, either through the function calls,
+or using the `ltac1val` quotation. The latter parses the same as `ltac1`, but
+has type `Ltac2.Ltac1.t` instead of `unit`, and dynamically behaves as an Ltac1
+thunk, i.e. `ltac1val:(foo)` corresponds to the tactic closure that Ltac1
+would generate from `idtac; foo`.
+
+Due to intricate dynamic semantics, understanding when Ltac1 value quotations
+focus is very hard. This is why some functions return a continuation-passing
+style value, as it can dispatch dynamically between focused and unfocused
+behaviour.
+
+Ltac2 from Ltac1
+~~~~~~~~~~~~~~~~
+
+Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation
+instead.
+
+Note that the tactic expression is evaluated eagerly, if one wants to use it as
+an argument to a Ltac1 function, she has to resort to the good old
+:n:`idtac; ltac2:(foo)` trick. For instance, the code below will fail immediately
+and won't print anything.
+
+.. coqtop:: in
+
+   From Ltac2 Require Import Ltac2.
+   Set Default Proof Mode "Classic".
+
+.. coqtop:: all
+
+   Ltac mytac tac := idtac "wow"; tac.
+
+   Goal True.
+   Proof.
+   Fail mytac ltac2:(fail).
+
+Transition from Ltac1
+---------------------
+
+Owing to the use of a lot of notations, the transition should not be too
+difficult. In particular, it should be possible to do it incrementally. That
+said, we do *not* guarantee you it is going to be a blissful walk either.
+Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with Coq
+will help you.
+
+We list the major changes and the transition strategies hereafter.
+
+Syntax changes
+~~~~~~~~~~~~~~
+
+Due to conflicts, a few syntactic rules have changed.
+
+- The dispatch tactical :n:`tac; [foo|bar]` is now written :n:`tac > [foo|bar]`.
+- Levels of a few operators have been revised. Some tacticals now parse as if
+  they were a normal function, i.e. one has to put parentheses around the
+  argument when it is complex, e.g an abstraction. List of affected tacticals:
+  :n:`try`, :n:`repeat`, :n:`do`, :n:`once`, :n:`progress`, :n:`time`, :n:`abstract`.
+- :n:`idtac` is no more. Either use :n:`()` if you expect nothing to happen,
+  :n:`(fun () => ())` if you want a thunk (see next section), or use printing
+  primitives from the :n:`Message` module if you want to display something.
+
+Tactic delay
+~~~~~~~~~~~~
+
+Tactics are not magically delayed anymore, neither as functions nor as
+arguments. It is your responsibility to thunk them beforehand and apply them
+at the call site.
+
+A typical example of a delayed function:
+
+:n:`Ltac foo := blah.`
+
+becomes
+
+:n:`Ltac2 foo () := blah.`
+
+All subsequent calls to `foo` must be applied to perform the same effect as
+before.
+
+Likewise, for arguments:
+
+:n:`Ltac bar tac := tac; tac; tac.`
+
+becomes
+
+:n:`Ltac2 bar tac := tac (); tac (); tac ().`
+
+We recommend the use of syntactic notations to ease the transition. For
+instance, the first example can alternatively be written as:
+
+:n:`Ltac2 foo0 () := blah.`
+:n:`Ltac2 Notation foo := foo0 ().`
+
+This allows to keep the subsequent calls to the tactic as-is, as the
+expression `foo` will be implicitly expanded everywhere into `foo0 ()`. Such
+a trick also works for arguments, as arguments of syntactic notations are
+implicitly thunked. The second example could thus be written as follows.
+
+:n:`Ltac2 bar0 tac := tac (); tac (); tac ().`
+:n:`Ltac2 Notation bar := bar0.`
+
+Variable binding
+~~~~~~~~~~~~~~~~
+
+Ltac1 relies on complex dynamic trickery to be able to tell apart bound
+variables from terms, hypotheses, etc. There is no such thing in Ltac2,
+as variables are recognized statically and other constructions do not live in
+the same syntactic world. Due to the abuse of quotations, it can sometimes be
+complicated to know what a mere identifier represents in a tactic expression. We
+recommend tracking the context and letting the compiler print typing errors to
+understand what is going on.
+
+We list below the typical changes one has to perform depending on the static
+errors produced by the typechecker.
+
+In Ltac expressions
++++++++++++++++++++
+
+.. exn:: Unbound ( value | constructor ) X
+
+   * if `X` is meant to be a term from the current stactic environment, replace
+     the problematic use by `'X`.
+   * if `X` is meant to be a hypothesis from the goal context, replace the
+     problematic use by `&X`.
+
+In quotations
++++++++++++++
+
+.. exn:: The reference X was not found in the current environment
+
+   * if `X` is meant to be a tactic expression bound by a Ltac2 let or function,
+     replace the problematic use by `$X`.
+   * if `X` is meant to be a hypothesis from the goal context, replace the
+     problematic use by `&X`.
+
+Exception catching
+~~~~~~~~~~~~~~~~~~
+
+Ltac2 features a proper exception-catching mechanism. For this reason, the
+Ltac1 mechanism relying on `fail` taking integers, and tacticals decreasing it,
+has been removed. Now exceptions are preserved by all tacticals, and it is
+your duty to catch them and reraise them depending on your use.
diff --git a/dune b/dune
index 787c3c3674..4beba1c14f 100644
--- a/dune
+++ b/dune
@@ -18,8 +18,9 @@
  (targets .vfiles.d)
  (deps
   (source_tree theories)
-  (source_tree plugins))
- (action (with-stdout-to .vfiles.d (bash "%{bin:coqdep} -dyndep both -noglob -boot `find theories plugins -type f -name *.v`"))))
+  (source_tree plugins)
+  (source_tree user-contrib))
+ (action (with-stdout-to .vfiles.d (bash "%{bin:coqdep} -dyndep both -noglob -boot `find theories plugins user-contrib -type f -name *.v`"))))
 
 (alias
  (name vodeps)
diff --git a/test-suite/Makefile b/test-suite/Makefile
index ba591ede20..94011447d7 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -99,7 +99,7 @@ INTERACTIVE := interactive
 UNIT_TESTS := unit-tests
 VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \
-  coqdoc ssr arithmetic
+  coqdoc ssr arithmetic ltac2
 
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS)
@@ -181,6 +181,7 @@ summary:
 	  $(call summary_dir, "tools/ tests", tools); \
 	  $(call summary_dir, "Unit tests", unit-tests); \
 	  $(call summary_dir, "Machine arithmetic tests", arithmetic); \
+	  $(call summary_dir, "Ltac2 tests", ltac2); \
 	  nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
 	  nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
 	  nb_tests=`expr $$nb_success + $$nb_failure`; \
@@ -319,7 +320,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	} > "$@"
 
 ssr: $(wildcard ssr/*.v:%.v=%.v.log)
-$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v)): %.v.log: %.v $(PREREQUISITELOG)
+$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v ltac2/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods)"; \
diff --git a/vendor/Ltac2/tests/compat.v b/test-suite/ltac2/compat.v
index 489fa638e4..489fa638e4 100644
--- a/vendor/Ltac2/tests/compat.v
+++ b/test-suite/ltac2/compat.v
diff --git a/vendor/Ltac2/tests/errors.v b/test-suite/ltac2/errors.v
index c677f6af5d..c677f6af5d 100644
--- a/vendor/Ltac2/tests/errors.v
+++ b/test-suite/ltac2/errors.v
diff --git a/vendor/Ltac2/tests/example1.v b/test-suite/ltac2/example1.v
index 023791050f..023791050f 100644
--- a/vendor/Ltac2/tests/example1.v
+++ b/test-suite/ltac2/example1.v
diff --git a/vendor/Ltac2/tests/example2.v b/test-suite/ltac2/example2.v
index c953d25061..c953d25061 100644
--- a/vendor/Ltac2/tests/example2.v
+++ b/test-suite/ltac2/example2.v
diff --git a/vendor/Ltac2/tests/matching.v b/test-suite/ltac2/matching.v
index 4338cbd32f..4338cbd32f 100644
--- a/vendor/Ltac2/tests/matching.v
+++ b/test-suite/ltac2/matching.v
diff --git a/vendor/Ltac2/tests/quot.v b/test-suite/ltac2/quot.v
index 624c4ad0c1..624c4ad0c1 100644
--- a/vendor/Ltac2/tests/quot.v
+++ b/test-suite/ltac2/quot.v
diff --git a/vendor/Ltac2/tests/rebind.v b/test-suite/ltac2/rebind.v
index e1c20a2059..e1c20a2059 100644
--- a/vendor/Ltac2/tests/rebind.v
+++ b/test-suite/ltac2/rebind.v
diff --git a/vendor/Ltac2/tests/stuff/ltac2.v b/test-suite/ltac2/stuff/ltac2.v
index 370bc70d15..370bc70d15 100644
--- a/vendor/Ltac2/tests/stuff/ltac2.v
+++ b/test-suite/ltac2/stuff/ltac2.v
diff --git a/vendor/Ltac2/tests/tacticals.v b/test-suite/ltac2/tacticals.v
index 1a2fbcbb37..1a2fbcbb37 100644
--- a/vendor/Ltac2/tests/tacticals.v
+++ b/test-suite/ltac2/tacticals.v
diff --git a/vendor/Ltac2/tests/typing.v b/test-suite/ltac2/typing.v
index 9f18292716..9f18292716 100644
--- a/vendor/Ltac2/tests/typing.v
+++ b/test-suite/ltac2/typing.v
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index fa8b771a74..6ddc503542 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -214,7 +214,7 @@ let record_dune d ff =
   if Sys.file_exists sd && Sys.is_directory sd then
     let out = open_out (bpath [sd;"dune"]) in
     let fmt = formatter_of_out_channel out in
-    if List.nth d 0 = "plugins" then
+    if List.nth d 0 = "plugins" || List.nth d 0 = "user-contrib" then
       fprintf fmt "(include plugin_base.dune)@\n";
     out_install fmt d ff;
     List.iter (pp_dep d fmt) ff;
@@ -224,17 +224,20 @@ let record_dune d ff =
     eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd
 
 (* File Scanning *)
-let scan_mlg m d =
-  let dir = ["plugins"; d] in
+let scan_mlg ~root m d =
+  let dir = [root; d] in
   let m = DirMap.add dir [] m in
   let mlg = Sys.(List.filter (fun f -> Filename.(check_suffix f ".mlg"))
                    Array.(to_list @@ readdir (bpath dir))) in
-  List.fold_left (fun m f -> add_map_list ["plugins"; d] (MLG f) m) m mlg
+  List.fold_left (fun m f -> add_map_list [root; d] (MLG f) m) m mlg
 
-let scan_plugins m =
+let scan_dir ~root m =
   let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in
-  let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath ["plugins";f]) Array.(to_list @@ readdir "plugins")) in
-  List.fold_left scan_mlg m dirs
+  let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath [root;f]) Array.(to_list @@ readdir root)) in
+  List.fold_left (scan_mlg ~root) m dirs
+
+let scan_plugins m = scan_dir ~root:"plugins" m
+let scan_usercontrib m = scan_dir ~root:"user-contrib" m
 
 (* This will be removed when we drop support for Make *)
 let fix_cmo_cma file =
@@ -291,5 +294,6 @@ let exec_ifile f =
 let _ =
   exec_ifile (fun ic ->
       let map = scan_plugins DirMap.empty in
+      let map = scan_usercontrib map in
       let map = read_vfiles ic map in
       out_map map)
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 7114965a11..8823206252 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -529,6 +529,11 @@ let coqdep () =
     add_rec_dir_import add_known "plugins" ["Coq"];
     add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
     add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
+    let user = "user-contrib" in
+    if Sys.file_exists user then begin
+      add_rec_dir_no_import add_known user [];
+      add_rec_dir_no_import (fun _ -> add_caml_known) user [];
+    end;
   end else begin
     (* option_boot is actually always false in this branch *)
     Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg));
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index aa023e6986..a638906c11 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -17,6 +17,9 @@ open Coqdep_common
     options (see for instance [option_natdynlk] below).
 *)
 
+let split_period = Str.split (Str.regexp (Str.quote "."))
+let add_q_include path l = add_rec_dir_no_import add_known path (split_period l)
+
 let rec parse = function
   | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
   | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
@@ -33,6 +36,7 @@ let rec parse = function
        add_caml_dir r;
        norec_dirs := StrSet.add r !norec_dirs;
        parse ll
+  | "-Q" :: r :: ln :: ll -> add_q_include r ln; parse ll
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
 
diff --git a/vendor/Ltac2/theories/Array.v b/user-contrib/Ltac2/Array.v
index 11b64e3515..11b64e3515 100644
--- a/vendor/Ltac2/theories/Array.v
+++ b/user-contrib/Ltac2/Array.v
diff --git a/vendor/Ltac2/theories/Char.v b/user-contrib/Ltac2/Char.v
index 29fef60f2c..29fef60f2c 100644
--- a/vendor/Ltac2/theories/Char.v
+++ b/user-contrib/Ltac2/Char.v
diff --git a/vendor/Ltac2/theories/Constr.v b/user-contrib/Ltac2/Constr.v
index d8d222730e..d8d222730e 100644
--- a/vendor/Ltac2/theories/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
diff --git a/vendor/Ltac2/theories/Control.v b/user-contrib/Ltac2/Control.v
index 071c2ea8ce..071c2ea8ce 100644
--- a/vendor/Ltac2/theories/Control.v
+++ b/user-contrib/Ltac2/Control.v
diff --git a/vendor/Ltac2/theories/Env.v b/user-contrib/Ltac2/Env.v
index c9b250f4ba..4aa1718c9a 100644
--- a/vendor/Ltac2/theories/Env.v
+++ b/user-contrib/Ltac2/Env.v
@@ -6,8 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Ltac2.Init.
-Require Import Std.
+From Ltac2 Require Import Init Std.
 
 Ltac2 @ external get : ident list -> Std.reference option := "ltac2" "env_get".
 (** Returns the global reference corresponding to the absolute name given as
diff --git a/vendor/Ltac2/theories/Fresh.v b/user-contrib/Ltac2/Fresh.v
index 5e876bb077..5e876bb077 100644
--- a/vendor/Ltac2/theories/Fresh.v
+++ b/user-contrib/Ltac2/Fresh.v
diff --git a/vendor/Ltac2/theories/Ident.v b/user-contrib/Ltac2/Ident.v
index 55456afbe2..55456afbe2 100644
--- a/vendor/Ltac2/theories/Ident.v
+++ b/user-contrib/Ltac2/Ident.v
diff --git a/vendor/Ltac2/theories/Init.v b/user-contrib/Ltac2/Init.v
index 16e7d7a6f9..16e7d7a6f9 100644
--- a/vendor/Ltac2/theories/Init.v
+++ b/user-contrib/Ltac2/Init.v
diff --git a/vendor/Ltac2/theories/Int.v b/user-contrib/Ltac2/Int.v
index 0a90d757b6..0a90d757b6 100644
--- a/vendor/Ltac2/theories/Int.v
+++ b/user-contrib/Ltac2/Int.v
diff --git a/vendor/Ltac2/theories/Ltac1.v b/user-contrib/Ltac2/Ltac1.v
index c4e0b606d0..c4e0b606d0 100644
--- a/vendor/Ltac2/theories/Ltac1.v
+++ b/user-contrib/Ltac2/Ltac1.v
diff --git a/vendor/Ltac2/theories/Ltac2.v b/user-contrib/Ltac2/Ltac2.v
index ac90f63560..ac90f63560 100644
--- a/vendor/Ltac2/theories/Ltac2.v
+++ b/user-contrib/Ltac2/Ltac2.v
diff --git a/vendor/Ltac2/theories/Message.v b/user-contrib/Ltac2/Message.v
index 7bffe0746b..7bffe0746b 100644
--- a/vendor/Ltac2/theories/Message.v
+++ b/user-contrib/Ltac2/Message.v
diff --git a/vendor/Ltac2/theories/Notations.v b/user-contrib/Ltac2/Notations.v
index f4621656d6..0eab36df82 100644
--- a/vendor/Ltac2/theories/Notations.v
+++ b/user-contrib/Ltac2/Notations.v
@@ -550,18 +550,6 @@ Ltac2 Notation typeclasses_eauto := typeclasses_eauto.
 Ltac2 f_equal0 () := ltac1:(f_equal).
 Ltac2 Notation f_equal := f_equal0 ().
 
-(** Firstorder *)
-
-Ltac2 firstorder0 tac refs ids :=
-  let refs := default_list refs in
-  let ids := default_list ids in
-  Std.firstorder tac refs ids.
-
-Ltac2 Notation "firstorder"
-  tac(opt(thunk(tactic)))
-  refs(opt(seq("using", list1(reference, ","))))
-  ids(opt(seq("with", list1(ident)))) := firstorder0 tac refs ids.
-
 (** now *)
 
 Ltac2 now0 t := t (); ltac1:(easy).
diff --git a/vendor/Ltac2/theories/Pattern.v b/user-contrib/Ltac2/Pattern.v
index 8d1fb0cd8a..8d1fb0cd8a 100644
--- a/vendor/Ltac2/theories/Pattern.v
+++ b/user-contrib/Ltac2/Pattern.v
diff --git a/vendor/Ltac2/theories/Std.v b/user-contrib/Ltac2/Std.v
index 73b2ba02c4..6c3f465f33 100644
--- a/vendor/Ltac2/theories/Std.v
+++ b/user-contrib/Ltac2/Std.v
@@ -257,7 +257,3 @@ Ltac2 @ external new_auto : debug -> int option -> (unit -> constr) list -> iden
 Ltac2 @ external eauto : debug -> int option -> int option -> (unit -> constr) list -> ident list option -> unit := "ltac2" "tac_eauto".
 
 Ltac2 @ external typeclasses_eauto : strategy option -> int option -> ident list option -> unit := "ltac2" "tac_typeclasses_eauto".
-
-(** firstorder *)
-
-Ltac2 @ external firstorder : (unit -> unit) option -> reference list -> ident list -> unit := "ltac2" "tac_firstorder".
diff --git a/vendor/Ltac2/theories/String.v b/user-contrib/Ltac2/String.v
index 99e1dab76b..99e1dab76b 100644
--- a/vendor/Ltac2/theories/String.v
+++ b/user-contrib/Ltac2/String.v
diff --git a/vendor/Ltac2/src/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 0071dbb088..890ed76d52 100644
--- a/vendor/Ltac2/src/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -454,11 +454,11 @@ GRAMMAR EXTEND Gram
              tc = LIST1 simple_intropattern SEP "," ; ")" ->
              { CAst.make ~loc @@ QIntroAndPattern (CAst.make ~loc (si::tc)) }
       | "("; si = simple_intropattern; "&";
-	     tc = LIST1 simple_intropattern SEP "&" ; ")" ->
-	  (* (A & B & C) is translated into (A,(B,C)) *)
-	{ let rec pairify = function
-	    | ([]|[_]|[_;_]) as l -> CAst.make ~loc l
-	    | t::q ->
+             tc = LIST1 simple_intropattern SEP "&" ; ")" ->
+          (* (A & B & C) is translated into (A,(B,C)) *)
+        { let rec pairify = function
+            | ([]|[_]|[_;_]) as l -> CAst.make ~loc l
+            | t::q ->
               let q =
                 CAst.make ~loc @@
                   QIntroAction (CAst.make ~loc @@
@@ -466,7 +466,7 @@ GRAMMAR EXTEND Gram
                       QIntroAndPattern (pairify q)))
               in
               CAst.make ~loc [t; q]
-	  in CAst.make ~loc @@ QIntroAndPattern (pairify (si::tc)) } ] ]
+          in CAst.make ~loc @@ QIntroAndPattern (pairify (si::tc)) } ] ]
   ;
   equality_intropattern:
     [ [ "->" -> { CAst.make ~loc @@ QIntroRewrite true }
diff --git a/vendor/Ltac2/src/ltac2_plugin.mlpack b/user-contrib/Ltac2/ltac2_plugin.mlpack
index 2a25e825cb..2a25e825cb 100644
--- a/vendor/Ltac2/src/ltac2_plugin.mlpack
+++ b/user-contrib/Ltac2/ltac2_plugin.mlpack
diff --git a/user-contrib/Ltac2/plugin_base.dune b/user-contrib/Ltac2/plugin_base.dune
new file mode 100644
index 0000000000..711e9b95d3
--- /dev/null
+++ b/user-contrib/Ltac2/plugin_base.dune
@@ -0,0 +1,6 @@
+(library
+ (name ltac2_plugin)
+ (public_name coq.plugins.ltac2)
+ (synopsis "Coq's Ltac2 plugin")
+ (modules_without_implementation tac2expr tac2qexpr tac2types)
+ (libraries coq.plugins.ltac))
diff --git a/vendor/Ltac2/src/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index d7e7b91ee6..d7e7b91ee6 100644
--- a/vendor/Ltac2/src/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
diff --git a/vendor/Ltac2/src/tac2core.mli b/user-contrib/Ltac2/tac2core.mli
index 9fae65bb3e..9fae65bb3e 100644
--- a/vendor/Ltac2/src/tac2core.mli
+++ b/user-contrib/Ltac2/tac2core.mli
diff --git a/vendor/Ltac2/src/tac2dyn.ml b/user-contrib/Ltac2/tac2dyn.ml
index 896676f08b..896676f08b 100644
--- a/vendor/Ltac2/src/tac2dyn.ml
+++ b/user-contrib/Ltac2/tac2dyn.ml
diff --git a/vendor/Ltac2/src/tac2dyn.mli b/user-contrib/Ltac2/tac2dyn.mli
index e995296840..e995296840 100644
--- a/vendor/Ltac2/src/tac2dyn.mli
+++ b/user-contrib/Ltac2/tac2dyn.mli
diff --git a/vendor/Ltac2/src/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 9fd01426de..9fd01426de 100644
--- a/vendor/Ltac2/src/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
diff --git a/vendor/Ltac2/src/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index d493192bb3..d493192bb3 100644
--- a/vendor/Ltac2/src/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
diff --git a/vendor/Ltac2/src/tac2env.ml b/user-contrib/Ltac2/tac2env.ml
index 93ad57e97e..93ad57e97e 100644
--- a/vendor/Ltac2/src/tac2env.ml
+++ b/user-contrib/Ltac2/tac2env.ml
diff --git a/vendor/Ltac2/src/tac2env.mli b/user-contrib/Ltac2/tac2env.mli
index c7e87c5432..c7e87c5432 100644
--- a/vendor/Ltac2/src/tac2env.mli
+++ b/user-contrib/Ltac2/tac2env.mli
diff --git a/vendor/Ltac2/src/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli
index 1069d0bfa3..1069d0bfa3 100644
--- a/vendor/Ltac2/src/tac2expr.mli
+++ b/user-contrib/Ltac2/tac2expr.mli
diff --git a/vendor/Ltac2/src/tac2extffi.ml b/user-contrib/Ltac2/tac2extffi.ml
index 315c970f9e..315c970f9e 100644
--- a/vendor/Ltac2/src/tac2extffi.ml
+++ b/user-contrib/Ltac2/tac2extffi.ml
diff --git a/vendor/Ltac2/src/tac2extffi.mli b/user-contrib/Ltac2/tac2extffi.mli
index f5251c3d0d..f5251c3d0d 100644
--- a/vendor/Ltac2/src/tac2extffi.mli
+++ b/user-contrib/Ltac2/tac2extffi.mli
diff --git a/vendor/Ltac2/src/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml
index e3127ab9df..e3127ab9df 100644
--- a/vendor/Ltac2/src/tac2ffi.ml
+++ b/user-contrib/Ltac2/tac2ffi.ml
diff --git a/vendor/Ltac2/src/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli
index bfc93d99e6..bfc93d99e6 100644
--- a/vendor/Ltac2/src/tac2ffi.mli
+++ b/user-contrib/Ltac2/tac2ffi.mli
diff --git a/vendor/Ltac2/src/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index de99fb167f..de99fb167f 100644
--- a/vendor/Ltac2/src/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
diff --git a/vendor/Ltac2/src/tac2intern.mli b/user-contrib/Ltac2/tac2intern.mli
index d646b5cda5..d646b5cda5 100644
--- a/vendor/Ltac2/src/tac2intern.mli
+++ b/user-contrib/Ltac2/tac2intern.mli
diff --git a/vendor/Ltac2/src/tac2interp.ml b/user-contrib/Ltac2/tac2interp.ml
index b0f8083aeb..db779db471 100644
--- a/vendor/Ltac2/src/tac2interp.ml
+++ b/user-contrib/Ltac2/tac2interp.ml
@@ -164,7 +164,7 @@ and interp_case ist e cse0 cse1 =
     let ist = CArray.fold_left2 push_name ist ids args in
     interp ist e
 
-and interp_with ist e cse def = 
+and interp_with ist e cse def =
   let (kn, args) = Tac2ffi.to_open e in
   let br = try Some (KNmap.find kn cse) with Not_found -> None in
   begin match br with
diff --git a/vendor/Ltac2/src/tac2interp.mli b/user-contrib/Ltac2/tac2interp.mli
index 21fdcd03af..21fdcd03af 100644
--- a/vendor/Ltac2/src/tac2interp.mli
+++ b/user-contrib/Ltac2/tac2interp.mli
diff --git a/vendor/Ltac2/src/tac2match.ml b/user-contrib/Ltac2/tac2match.ml
index c9e549d47e..058d02adde 100644
--- a/vendor/Ltac2/src/tac2match.ml
+++ b/user-contrib/Ltac2/tac2match.ml
@@ -49,7 +49,7 @@ let is_empty_subst = Id.Map.is_empty
    would ensure consistency. *)
 let equal_instances env sigma c1 c2 =
   (* How to compare instances? Do we want the terms to be convertible?
-     unifiable? Do we want the universe levels to be relevant? 
+     unifiable? Do we want the universe levels to be relevant?
      (historically, conv_x is used) *)
   Reductionops.is_conv env sigma c1 c2
 
@@ -152,10 +152,10 @@ module PatternMatching (E:StaticEnvironment) = struct
 
   (** {6 Pattern-matching} *)
 
-  let pattern_match_term pat term = 
+  let pattern_match_term pat term =
     match pat with
     | MatchPattern p ->
-        begin 
+        begin
           try
             put_subst (Constr_matching.matches E.env E.sigma p term) <*>
             return None
diff --git a/vendor/Ltac2/src/tac2match.mli b/user-contrib/Ltac2/tac2match.mli
index c82c40d238..c82c40d238 100644
--- a/vendor/Ltac2/src/tac2match.mli
+++ b/user-contrib/Ltac2/tac2match.mli
diff --git a/vendor/Ltac2/src/tac2print.ml b/user-contrib/Ltac2/tac2print.ml
index f4cb290265..f4cb290265 100644
--- a/vendor/Ltac2/src/tac2print.ml
+++ b/user-contrib/Ltac2/tac2print.ml
diff --git a/vendor/Ltac2/src/tac2print.mli b/user-contrib/Ltac2/tac2print.mli
index 9b9db2937d..9b9db2937d 100644
--- a/vendor/Ltac2/src/tac2print.mli
+++ b/user-contrib/Ltac2/tac2print.mli
diff --git a/vendor/Ltac2/src/tac2qexpr.mli b/user-contrib/Ltac2/tac2qexpr.mli
index 400ab1a092..400ab1a092 100644
--- a/vendor/Ltac2/src/tac2qexpr.mli
+++ b/user-contrib/Ltac2/tac2qexpr.mli
diff --git a/vendor/Ltac2/src/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml
index a98264745e..a98264745e 100644
--- a/vendor/Ltac2/src/tac2quote.ml
+++ b/user-contrib/Ltac2/tac2quote.ml
diff --git a/vendor/Ltac2/src/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli
index 1b03dad8ec..1b03dad8ec 100644
--- a/vendor/Ltac2/src/tac2quote.mli
+++ b/user-contrib/Ltac2/tac2quote.mli
diff --git a/vendor/Ltac2/src/tac2stdlib.ml b/user-contrib/Ltac2/tac2stdlib.ml
index ffef2c05fd..fb51fc965b 100644
--- a/vendor/Ltac2/src/tac2stdlib.ml
+++ b/user-contrib/Ltac2/tac2stdlib.ml
@@ -570,9 +570,3 @@ end
 let () = define_prim3 "tac_typeclasses_eauto" (option strategy) (option int) (option (list ident)) begin fun str n dbs ->
   Tac2tactics.typeclasses_eauto str n dbs
 end
-
-(** Firstorder *)
-
-let () = define_prim3 "tac_firstorder" (option (thunk unit)) (list reference) (list ident) begin fun tac refs ids ->
-  Tac2tactics.firstorder tac refs ids
-end
diff --git a/vendor/Ltac2/src/tac2stdlib.mli b/user-contrib/Ltac2/tac2stdlib.mli
index 927b57074d..927b57074d 100644
--- a/vendor/Ltac2/src/tac2stdlib.mli
+++ b/user-contrib/Ltac2/tac2stdlib.mli
diff --git a/vendor/Ltac2/src/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index ce37a613b1..603e00c815 100644
--- a/vendor/Ltac2/src/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -445,11 +445,3 @@ let inversion knd arg pat ids =
 let contradiction c =
   let c = Option.map mk_with_bindings c in
   Contradiction.contradiction c
-
-(** Firstorder *)
-
-let firstorder tac refs ids =
-  let open Ground_plugin in
-  let ids = List.map Id.to_string ids in
-  let tac = Option.map (fun tac -> thaw Tac2ffi.unit tac) tac in
-  G_ground.gen_ground_tac true tac refs ids
diff --git a/vendor/Ltac2/src/tac2tactics.mli b/user-contrib/Ltac2/tac2tactics.mli
index 026673acbf..e56544cd68 100644
--- a/vendor/Ltac2/src/tac2tactics.mli
+++ b/user-contrib/Ltac2/tac2tactics.mli
@@ -120,5 +120,3 @@ val typeclasses_eauto : Class_tactics.search_strategy option -> int option ->
 val inversion : Inv.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
 
 val contradiction : constr_with_bindings option -> unit tactic
-
-val firstorder : unit thunk option -> GlobRef.t list -> Id.t list -> unit tactic
diff --git a/vendor/Ltac2/src/tac2types.mli b/user-contrib/Ltac2/tac2types.mli
index fa31153a27..fa31153a27 100644
--- a/vendor/Ltac2/src/tac2types.mli
+++ b/user-contrib/Ltac2/tac2types.mli
diff --git a/vendor/Ltac2/.gitignore b/vendor/Ltac2/.gitignore
deleted file mode 100644
index 00e15f8daa..0000000000
--- a/vendor/Ltac2/.gitignore
+++ /dev/null
@@ -1,18 +0,0 @@
-Makefile.coq
-Makefile.coq.conf
-*.glob
-*.d
-*.d.raw
-*.vio
-*.vo
-*.cm*
-*.annot
-*.spit
-*.spot
-*.o
-*.a
-*.aux
-tests/*.log
-*.install
-_build
-.merlin
diff --git a/vendor/Ltac2/.travis.yml b/vendor/Ltac2/.travis.yml
deleted file mode 100644
index 2628abde45..0000000000
--- a/vendor/Ltac2/.travis.yml
+++ /dev/null
@@ -1,40 +0,0 @@
-dist: trusty
-sudo: required
-language: generic
-
-services:
-  - docker
-
-env:
-  global:
-  - NJOBS="2"
-  - CONTRIB_NAME="ltac2"
-  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 update -y
-    # opam install -y -j ${NJOBS} coq-mathcomp-ssreflect
-    opam config list
-    opam repo list
-    opam list
-    "
-script:
-- echo -e "${ANSI_YELLOW}Building ${CONTRIB_NAME}...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\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}
-    make
-    make tests
-    "
-- docker stop COQ  # optional
-- echo -en 'travis_fold:end:script\\r'
diff --git a/vendor/Ltac2/LICENSE b/vendor/Ltac2/LICENSE
deleted file mode 100644
index 27950e8d20..0000000000
--- a/vendor/Ltac2/LICENSE
+++ /dev/null
@@ -1,458 +0,0 @@
-		  GNU LESSER GENERAL PUBLIC LICENSE
-		       Version 2.1, February 1999
-
- Copyright (C) 1991, 1999 Free Software Foundation, Inc.
-     59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
- Everyone is permitted to copy and distribute verbatim copies
- of this license document, but changing it is not allowed.
-
-[This is the first released version of the Lesser GPL.  It also counts
- as the successor of the GNU Library Public License, version 2, hence
- the version number 2.1.]
-
-			    Preamble
-
-  The licenses for most software are designed to take away your
-freedom to share and change it.  By contrast, the GNU General Public
-Licenses are intended to guarantee your freedom to share and change
-free software--to make sure the software is free for all its users.
-
-  This license, the Lesser General Public License, applies to some
-specially designated software packages--typically libraries--of the
-Free Software Foundation and other authors who decide to use it.  You
-can use it too, but we suggest you first think carefully about whether
-this license or the ordinary General Public License is the better
-strategy to use in any particular case, based on the explanations below.
-
-  When we speak of free software, we are referring to freedom of use,
-not price.  Our General Public Licenses are designed to make sure that
-you have the freedom to distribute copies of free software (and charge
-for this service if you wish); that you receive source code or can get
-it if you want it; that you can change the software and use pieces of
-it in new free programs; and that you are informed that you can do
-these things.
-
-  To protect your rights, we need to make restrictions that forbid
-distributors to deny you these rights or to ask you to surrender these
-rights.  These restrictions translate to certain responsibilities for
-you if you distribute copies of the library or if you modify it.
-
-  For example, if you distribute copies of the library, whether gratis
-or for a fee, you must give the recipients all the rights that we gave
-you.  You must make sure that they, too, receive or can get the source
-code.  If you link other code with the library, you must provide
-complete object files to the recipients, so that they can relink them
-with the library after making changes to the library and recompiling
-it.  And you must show them these terms so they know their rights.
-
-  We protect your rights with a two-step method: (1) we copyright the
-library, and (2) we offer you this license, which gives you legal
-permission to copy, distribute and/or modify the library.
-
-  To protect each distributor, we want to make it very clear that
-there is no warranty for the free library.  Also, if the library is
-modified by someone else and passed on, the recipients should know
-that what they have is not the original version, so that the original
-author's reputation will not be affected by problems that might be
-introduced by others.
-
-  Finally, software patents pose a constant threat to the existence of
-any free program.  We wish to make sure that a company cannot
-effectively restrict the users of a free program by obtaining a
-restrictive license from a patent holder.  Therefore, we insist that
-any patent license obtained for a version of the library must be
-consistent with the full freedom of use specified in this license.
-
-  Most GNU software, including some libraries, is covered by the
-ordinary GNU General Public License.  This license, the GNU Lesser
-General Public License, applies to certain designated libraries, and
-is quite different from the ordinary General Public License.  We use
-this license for certain libraries in order to permit linking those
-libraries into non-free programs.
-
-  When a program is linked with a library, whether statically or using
-a shared library, the combination of the two is legally speaking a
-combined work, a derivative of the original library.  The ordinary
-General Public License therefore permits such linking only if the
-entire combination fits its criteria of freedom.  The Lesser General
-Public License permits more lax criteria for linking other code with
-the library.
-
-  We call this license the "Lesser" General Public License because it
-does Less to protect the user's freedom than the ordinary General
-Public License.  It also provides other free software developers Less
-of an advantage over competing non-free programs.  These disadvantages
-are the reason we use the ordinary General Public License for many
-libraries.  However, the Lesser license provides advantages in certain
-special circumstances.
-
-  For example, on rare occasions, there may be a special need to
-encourage the widest possible use of a certain library, so that it becomes
-a de-facto standard.  To achieve this, non-free programs must be
-allowed to use the library.  A more frequent case is that a free
-library does the same job as widely used non-free libraries.  In this
-case, there is little to gain by limiting the free library to free
-software only, so we use the Lesser General Public License.
-
-  In other cases, permission to use a particular library in non-free
-programs enables a greater number of people to use a large body of
-free software.  For example, permission to use the GNU C Library in
-non-free programs enables many more people to use the whole GNU
-operating system, as well as its variant, the GNU/Linux operating
-system.
-
-  Although the Lesser General Public License is Less protective of the
-users' freedom, it does ensure that the user of a program that is
-linked with the Library has the freedom and the wherewithal to run
-that program using a modified version of the Library.
-
-  The precise terms and conditions for copying, distribution and
-modification follow.  Pay close attention to the difference between a
-"work based on the library" and a "work that uses the library".  The
-former contains code derived from the library, whereas the latter must
-be combined with the library in order to run.
-
-		  GNU LESSER GENERAL PUBLIC LICENSE
-   TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
-
-  0. This License Agreement applies to any software library or other
-program which contains a notice placed by the copyright holder or
-other authorized party saying it may be distributed under the terms of
-this Lesser General Public License (also called "this License").
-Each licensee is addressed as "you".
-
-  A "library" means a collection of software functions and/or data
-prepared so as to be conveniently linked with application programs
-(which use some of those functions and data) to form executables.
-
-  The "Library", below, refers to any such software library or work
-which has been distributed under these terms.  A "work based on the
-Library" means either the Library or any derivative work under
-copyright law: that is to say, a work containing the Library or a
-portion of it, either verbatim or with modifications and/or translated
-straightforwardly into another language.  (Hereinafter, translation is
-included without limitation in the term "modification".)
-
-  "Source code" for a work means the preferred form of the work for
-making modifications to it.  For a library, complete source code means
-all the source code for all modules it contains, plus any associated
-interface definition files, plus the scripts used to control compilation
-and installation of the library.
-
-  Activities other than copying, distribution and modification are not
-covered by this License; they are outside its scope.  The act of
-running a program using the Library is not restricted, and output from
-such a program is covered only if its contents constitute a work based
-on the Library (independent of the use of the Library in a tool for
-writing it).  Whether that is true depends on what the Library does
-and what the program that uses the Library does.
-  
-  1. You may copy and distribute verbatim copies of the Library's
-complete source code as you receive it, in any medium, provided that
-you conspicuously and appropriately publish on each copy an
-appropriate copyright notice and disclaimer of warranty; keep intact
-all the notices that refer to this License and to the absence of any
-warranty; and distribute a copy of this License along with the
-Library.
-
-  You may charge a fee for the physical act of transferring a copy,
-and you may at your option offer warranty protection in exchange for a
-fee.
-
-  2. You may modify your copy or copies of the Library or any portion
-of it, thus forming a work based on the Library, and copy and
-distribute such modifications or work under the terms of Section 1
-above, provided that you also meet all of these conditions:
-
-    a) The modified work must itself be a software library.
-
-    b) You must cause the files modified to carry prominent notices
-    stating that you changed the files and the date of any change.
-
-    c) You must cause the whole of the work to be licensed at no
-    charge to all third parties under the terms of this License.
-
-    d) If a facility in the modified Library refers to a function or a
-    table of data to be supplied by an application program that uses
-    the facility, other than as an argument passed when the facility
-    is invoked, then you must make a good faith effort to ensure that,
-    in the event an application does not supply such function or
-    table, the facility still operates, and performs whatever part of
-    its purpose remains meaningful.
-
-    (For example, a function in a library to compute square roots has
-    a purpose that is entirely well-defined independent of the
-    application.  Therefore, Subsection 2d requires that any
-    application-supplied function or table used by this function must
-    be optional: if the application does not supply it, the square
-    root function must still compute square roots.)
-
-These requirements apply to the modified work as a whole.  If
-identifiable sections of that work are not derived from the Library,
-and can be reasonably considered independent and separate works in
-themselves, then this License, and its terms, do not apply to those
-sections when you distribute them as separate works.  But when you
-distribute the same sections as part of a whole which is a work based
-on the Library, the distribution of the whole must be on the terms of
-this License, whose permissions for other licensees extend to the
-entire whole, and thus to each and every part regardless of who wrote
-it.
-
-Thus, it is not the intent of this section to claim rights or contest
-your rights to work written entirely by you; rather, the intent is to
-exercise the right to control the distribution of derivative or
-collective works based on the Library.
-
-In addition, mere aggregation of another work not based on the Library
-with the Library (or with a work based on the Library) on a volume of
-a storage or distribution medium does not bring the other work under
-the scope of this License.
-
-  3. You may opt to apply the terms of the ordinary GNU General Public
-License instead of this License to a given copy of the Library.  To do
-this, you must alter all the notices that refer to this License, so
-that they refer to the ordinary GNU General Public License, version 2,
-instead of to this License.  (If a newer version than version 2 of the
-ordinary GNU General Public License has appeared, then you can specify
-that version instead if you wish.)  Do not make any other change in
-these notices.
-
-  Once this change is made in a given copy, it is irreversible for
-that copy, so the ordinary GNU General Public License applies to all
-subsequent copies and derivative works made from that copy.
-
-  This option is useful when you wish to copy part of the code of
-the Library into a program that is not a library.
-
-  4. You may copy and distribute the Library (or a portion or
-derivative of it, under Section 2) in object code or executable form
-under the terms of Sections 1 and 2 above provided that you accompany
-it with the complete corresponding machine-readable source code, which
-must be distributed under the terms of Sections 1 and 2 above on a
-medium customarily used for software interchange.
-
-  If distribution of object code is made by offering access to copy
-from a designated place, then offering equivalent access to copy the
-source code from the same place satisfies the requirement to
-distribute the source code, even though third parties are not
-compelled to copy the source along with the object code.
-
-  5. A program that contains no derivative of any portion of the
-Library, but is designed to work with the Library by being compiled or
-linked with it, is called a "work that uses the Library".  Such a
-work, in isolation, is not a derivative work of the Library, and
-therefore falls outside the scope of this License.
-
-  However, linking a "work that uses the Library" with the Library
-creates an executable that is a derivative of the Library (because it
-contains portions of the Library), rather than a "work that uses the
-library".  The executable is therefore covered by this License.
-Section 6 states terms for distribution of such executables.
-
-  When a "work that uses the Library" uses material from a header file
-that is part of the Library, the object code for the work may be a
-derivative work of the Library even though the source code is not.
-Whether this is true is especially significant if the work can be
-linked without the Library, or if the work is itself a library.  The
-threshold for this to be true is not precisely defined by law.
-
-  If such an object file uses only numerical parameters, data
-structure layouts and accessors, and small macros and small inline
-functions (ten lines or less in length), then the use of the object
-file is unrestricted, regardless of whether it is legally a derivative
-work.  (Executables containing this object code plus portions of the
-Library will still fall under Section 6.)
-
-  Otherwise, if the work is a derivative of the Library, you may
-distribute the object code for the work under the terms of Section 6.
-Any executables containing that work also fall under Section 6,
-whether or not they are linked directly with the Library itself.
-
-  6. As an exception to the Sections above, you may also combine or
-link a "work that uses the Library" with the Library to produce a
-work containing portions of the Library, and distribute that work
-under terms of your choice, provided that the terms permit
-modification of the work for the customer's own use and reverse
-engineering for debugging such modifications.
-
-  You must give prominent notice with each copy of the work that the
-Library is used in it and that the Library and its use are covered by
-this License.  You must supply a copy of this License.  If the work
-during execution displays copyright notices, you must include the
-copyright notice for the Library among them, as well as a reference
-directing the user to the copy of this License.  Also, you must do one
-of these things:
-
-    a) Accompany the work with the complete corresponding
-    machine-readable source code for the Library including whatever
-    changes were used in the work (which must be distributed under
-    Sections 1 and 2 above); and, if the work is an executable linked
-    with the Library, with the complete machine-readable "work that
-    uses the Library", as object code and/or source code, so that the
-    user can modify the Library and then relink to produce a modified
-    executable containing the modified Library.  (It is understood
-    that the user who changes the contents of definitions files in the
-    Library will not necessarily be able to recompile the application
-    to use the modified definitions.)
-
-    b) Use a suitable shared library mechanism for linking with the
-    Library.  A suitable mechanism is one that (1) uses at run time a
-    copy of the library already present on the user's computer system,
-    rather than copying library functions into the executable, and (2)
-    will operate properly with a modified version of the library, if
-    the user installs one, as long as the modified version is
-    interface-compatible with the version that the work was made with.
-
-    c) Accompany the work with a written offer, valid for at
-    least three years, to give the same user the materials
-    specified in Subsection 6a, above, for a charge no more
-    than the cost of performing this distribution.
-
-    d) If distribution of the work is made by offering access to copy
-    from a designated place, offer equivalent access to copy the above
-    specified materials from the same place.
-
-    e) Verify that the user has already received a copy of these
-    materials or that you have already sent this user a copy.
-
-  For an executable, the required form of the "work that uses the
-Library" must include any data and utility programs needed for
-reproducing the executable from it.  However, as a special exception,
-the materials to be distributed need not include anything that is
-normally distributed (in either source or binary form) with the major
-components (compiler, kernel, and so on) of the operating system on
-which the executable runs, unless that component itself accompanies
-the executable.
-
-  It may happen that this requirement contradicts the license
-restrictions of other proprietary libraries that do not normally
-accompany the operating system.  Such a contradiction means you cannot
-use both them and the Library together in an executable that you
-distribute.
-
-  7. You may place library facilities that are a work based on the
-Library side-by-side in a single library together with other library
-facilities not covered by this License, and distribute such a combined
-library, provided that the separate distribution of the work based on
-the Library and of the other library facilities is otherwise
-permitted, and provided that you do these two things:
-
-    a) Accompany the combined library with a copy of the same work
-    based on the Library, uncombined with any other library
-    facilities.  This must be distributed under the terms of the
-    Sections above.
-
-    b) Give prominent notice with the combined library of the fact
-    that part of it is a work based on the Library, and explaining
-    where to find the accompanying uncombined form of the same work.
-
-  8. You may not copy, modify, sublicense, link with, or distribute
-the Library except as expressly provided under this License.  Any
-attempt otherwise to copy, modify, sublicense, link with, or
-distribute the Library is void, and will automatically terminate your
-rights under this License.  However, parties who have received copies,
-or rights, from you under this License will not have their licenses
-terminated so long as such parties remain in full compliance.
-
-  9. You are not required to accept this License, since you have not
-signed it.  However, nothing else grants you permission to modify or
-distribute the Library or its derivative works.  These actions are
-prohibited by law if you do not accept this License.  Therefore, by
-modifying or distributing the Library (or any work based on the
-Library), you indicate your acceptance of this License to do so, and
-all its terms and conditions for copying, distributing or modifying
-the Library or works based on it.
-
-  10. Each time you redistribute the Library (or any work based on the
-Library), the recipient automatically receives a license from the
-original licensor to copy, distribute, link with or modify the Library
-subject to these terms and conditions.  You may not impose any further
-restrictions on the recipients' exercise of the rights granted herein.
-You are not responsible for enforcing compliance by third parties with
-this License.
-
-  11. If, as a consequence of a court judgment or allegation of patent
-infringement or for any other reason (not limited to patent issues),
-conditions are imposed on you (whether by court order, agreement or
-otherwise) that contradict the conditions of this License, they do not
-excuse you from the conditions of this License.  If you cannot
-distribute so as to satisfy simultaneously your obligations under this
-License and any other pertinent obligations, then as a consequence you
-may not distribute the Library at all.  For example, if a patent
-license would not permit royalty-free redistribution of the Library by
-all those who receive copies directly or indirectly through you, then
-the only way you could satisfy both it and this License would be to
-refrain entirely from distribution of the Library.
-
-If any portion of this section is held invalid or unenforceable under any
-particular circumstance, the balance of the section is intended to apply,
-and the section as a whole is intended to apply in other circumstances.
-
-It is not the purpose of this section to induce you to infringe any
-patents or other property right claims or to contest validity of any
-such claims; this section has the sole purpose of protecting the
-integrity of the free software distribution system which is
-implemented by public license practices.  Many people have made
-generous contributions to the wide range of software distributed
-through that system in reliance on consistent application of that
-system; it is up to the author/donor to decide if he or she is willing
-to distribute software through any other system and a licensee cannot
-impose that choice.
-
-This section is intended to make thoroughly clear what is believed to
-be a consequence of the rest of this License.
-
-  12. If the distribution and/or use of the Library is restricted in
-certain countries either by patents or by copyrighted interfaces, the
-original copyright holder who places the Library under this License may add
-an explicit geographical distribution limitation excluding those countries,
-so that distribution is permitted only in or among countries not thus
-excluded.  In such case, this License incorporates the limitation as if
-written in the body of this License.
-
-  13. The Free Software Foundation may publish revised and/or new
-versions of the Lesser General Public License from time to time.
-Such new versions will be similar in spirit to the present version,
-but may differ in detail to address new problems or concerns.
-
-Each version is given a distinguishing version number.  If the Library
-specifies a version number of this License which applies to it and
-"any later version", you have the option of following the terms and
-conditions either of that version or of any later version published by
-the Free Software Foundation.  If the Library does not specify a
-license version number, you may choose any version ever published by
-the Free Software Foundation.
-
-  14. If you wish to incorporate parts of the Library into other free
-programs whose distribution conditions are incompatible with these,
-write to the author to ask for permission.  For software which is
-copyrighted by the Free Software Foundation, write to the Free
-Software Foundation; we sometimes make exceptions for this.  Our
-decision will be guided by the two goals of preserving the free status
-of all derivatives of our free software and of promoting the sharing
-and reuse of software generally.
-
-			    NO WARRANTY
-
-  15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO
-WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE LAW.
-EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR
-OTHER PARTIES PROVIDE THE LIBRARY "AS IS" WITHOUT WARRANTY OF ANY
-KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE
-IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
-PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
-LIBRARY IS WITH YOU.  SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME
-THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
-
-  16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN
-WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY
-AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE LIABLE TO YOU
-FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR
-CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE
-LIBRARY (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING
-RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A
-FAILURE OF THE LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF
-SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH
-DAMAGES.
-
-		     END OF TERMS AND CONDITIONS
diff --git a/vendor/Ltac2/Makefile b/vendor/Ltac2/Makefile
deleted file mode 100644
index e0e197650d..0000000000
--- a/vendor/Ltac2/Makefile
+++ /dev/null
@@ -1,14 +0,0 @@
-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/vendor/Ltac2/README.md b/vendor/Ltac2/README.md
deleted file mode 100644
index d49dd88076..0000000000
--- a/vendor/Ltac2/README.md
+++ /dev/null
@@ -1,25 +0,0 @@
-[![Build Status](https://travis-ci.org/ppedrot/ltac2.svg?branch=master)](https://travis-ci.org/ppedrot/ltac2)
-
-Overview
-========
-
-This is a standalone version of the Ltac2 plugin. Ltac2 is an attempt at
-providing the Coq users with a tactic language that is more robust and more
-expressive than the venerable Ltac language.
-
-Status
-========
-
-It is mostly a toy to experiment for now, and the implementation is quite
-bug-ridden. Don't mistake this for a final product!
-
-Installation
-============
-
-This should compile with Coq master, assuming the `COQBIN` variable is set
-correctly. Standard procedures for `coq_makefile`-generated plugins apply.
-
-Demo
-====
-
-Horrible test-files are provided in the `tests` folder. Not for kids.
diff --git a/vendor/Ltac2/_CoqProject b/vendor/Ltac2/_CoqProject
deleted file mode 100644
index dda5a8001a..0000000000
--- a/vendor/Ltac2/_CoqProject
+++ /dev/null
@@ -1,51 +0,0 @@
--R theories/ Ltac2
--I src/
-
-src/tac2dyn.ml
-src/tac2dyn.mli
-src/tac2expr.mli
-src/tac2types.mli
-src/tac2env.ml
-src/tac2env.mli
-src/tac2print.ml
-src/tac2print.mli
-src/tac2intern.ml
-src/tac2intern.mli
-src/tac2interp.ml
-src/tac2interp.mli
-src/tac2entries.ml
-src/tac2entries.mli
-src/tac2ffi.ml
-src/tac2ffi.mli
-src/tac2qexpr.mli
-src/tac2quote.ml
-src/tac2quote.mli
-src/tac2match.ml
-src/tac2match.mli
-src/tac2core.ml
-src/tac2core.mli
-src/tac2extffi.ml
-src/tac2extffi.mli
-src/tac2tactics.ml
-src/tac2tactics.mli
-src/tac2stdlib.ml
-src/tac2stdlib.mli
-src/g_ltac2.mlg
-src/ltac2_plugin.mlpack
-
-theories/Init.v
-theories/Int.v
-theories/Char.v
-theories/String.v
-theories/Ident.v
-theories/Array.v
-theories/Control.v
-theories/Message.v
-theories/Constr.v
-theories/Pattern.v
-theories/Fresh.v
-theories/Std.v
-theories/Env.v
-theories/Notations.v
-theories/Ltac1.v
-theories/Ltac2.v
diff --git a/vendor/Ltac2/doc/ltac2.md b/vendor/Ltac2/doc/ltac2.md
deleted file mode 100644
index b217cb08e6..0000000000
--- a/vendor/Ltac2/doc/ltac2.md
+++ /dev/null
@@ -1,1036 +0,0 @@
-# Summary
-
-The Ltac tactic language is probably one of the ingredients of the success of
-Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac:
-
-- has nothing like intended semantics
-- is very non-uniform due to organic growth
-- lacks expressivity and requires programming-by-hacking
-- is slow
-- is error-prone and fragile
-- has an intricate implementation
-
-This has a lot of terrible consequences, most notably the fact that it is never
-clear whether some observed behaviour is a bug or a proper one.
-
-Following the need of users that start developing huge projects relying 
-critically on Ltac, we believe that we should offer a proper modern language
-that features at least the following:
-
-- at least informal, predictable semantics
-- a typing system
-- standard programming facilities (i.e. datatypes)
-
-This document describes the implementation of such a language. The
-implementation of Ltac as of Coq 8.7 will be referred to as Ltac1.
-
-# Contents
-
-<!-- markdown-toc start - Don't edit this section. Run M-x markdown-toc-refresh-toc -->
-**Table of Contents**
-
-- [Summary](#summary)
-- [Contents](#contents)
-- [General design](#general-design)
-- [ML component](#ml-component)
-    - [Overview](#overview)
-    - [Type Syntax](#type-syntax)
-    - [Type declarations](#type-declarations)
-    - [Term Syntax](#term-syntax)
-    - [Ltac Definitions](#ltac-definitions)
-    - [Reduction](#reduction)
-    - [Typing](#typing)
-    - [Effects](#effects)
-        - [Standard IO](#standard-io)
-        - [Fatal errors](#fatal-errors)
-        - [Backtrack](#backtrack)
-        - [Goals](#goals)
-- [Meta-programming](#meta-programming)
-    - [Overview](#overview-1)
-    - [Generic Syntax for Quotations](#generic-syntax-for-quotations)
-        - [Built-in quotations](#built-in-quotations)
-        - [Strict vs. non-strict mode](#strict-vs-non-strict-mode)
-    - [Term Antiquotations](#term-antiquotations)
-        - [Syntax](#syntax)
-        - [Semantics](#semantics)
-            - [Static semantics](#static-semantics)
-            - [Dynamic semantics](#dynamic-semantics)
-    - [Trivial Term Antiquotations](#trivial-term-antiquotations)
-    - [Match over terms](#match-over-terms)
-    - [Match over goals](#match-over-goals)
-- [Notations](#notations)
-    - [Scopes](#scopes)
-    - [Notations](#notations-1)
-    - [Abbreviations](#abbreviations)
-- [Evaluation](#evaluation)
-- [Debug](#debug)
-- [Compatibility layer with Ltac1](#compatibility-layer-with-ltac1)
-    - [Ltac1 from Ltac2](#ltac1-from-ltac2)
-    - [Ltac2 from Ltac1](#ltac2-from-ltac1)
-- [Transition from Ltac1](#transition-from-ltac1)
-    - [Syntax changes](#syntax-changes)
-    - [Tactic delay](#tactic-delay)
-    - [Variable binding](#variable-binding)
-        - [In Ltac expressions](#in-ltac-expressions)
-        - [In quotations](#in-quotations)
-    - [Exception catching](#exception-catching)
-- [TODO](#todo)
-
-<!-- markdown-toc end -->
-
-
-# General design
-
-There are various alternatives to Ltac1, such that Mtac or Rtac for instance.
-While those alternatives can be quite distinct from Ltac1, we designed
-Ltac2 to be closest as reasonably possible to Ltac1, while fixing the
-aforementioned defects.
-
-In particular, Ltac2 is:
-- a member of the ML family of languages, i.e.
-  * a call-by-value functional language
-  * with effects
-  * together with Hindley-Milner type system
-- a language featuring meta-programming facilities for the manipulation of
-  Coq-side terms
-- a language featuring notation facilities to help writing palatable scripts
-
-We describe more in details each point in the remainder of this document.
-
-# ML component
-
-## Overview
-
-Ltac2 is a member of the ML family of languages, in the sense that it is an
-effectful call-by-value functional language, with static typing à la
-Hindley-Milner. It is commonly accepted that ML constitutes a sweet spot in PL
-design, as it is relatively expressive while not being either too lax
-(contrarily to dynamic typing) nor too strict (contrarily to say, dependent
-types).
-
-The main goal of Ltac2 is to serve as a meta-language for Coq. As such, it
-naturally fits in the ML lineage, just as the historical ML was designed as
-the tactic language for the LCF prover. It can also be seen as a general-purpose
-language, by simply forgetting about the Coq-specific features.
-
-Sticking to a standard ML type system can be considered somewhat weak for a
-meta-language designed to manipulate Coq terms. In particular, there is no
-way to statically guarantee that a Coq term resulting from an Ltac2
-computation will be well-typed. This is actually a design choice, motivated
-by retro-compatibility with Ltac1. Instead, well-typedness is deferred to
-dynamic checks, allowing many primitive functions to fail whenever they are
-provided with an ill-typed term.
-
-The language is naturally effectful as it manipulates the global state of the
-proof engine. This allows to think of proof-modifying primitives as effects
-in a straightforward way. Semantically, proof manipulation lives in a monad,
-which allows to ensure that Ltac2 satisfies the same equations as a generic ML
-with unspecified effects would do, e.g. function reduction is substitution
-by a value.
-
-## Type Syntax
-
-At the level of terms, we simply elaborate on Ltac1 syntax, which is quite
-close to e.g. the one of OCaml. Types follow the simply-typed syntax of OCaml.
-
-```
-TYPE :=
-| "(" TYPE₀ "," ... "," TYPEₙ ")" TYPECONST
-| "(" TYPE₀ "*" ... "*" TYPEₙ ")"
-| TYPE₁ "->" TYPE₂
-| TYPEVAR
-
-TYPECONST := ( MODPATH "." )* LIDENT
-
-TYPEVAR := "'" LIDENT
-
-TYPEPARAMS := "(" TYPEVAR₀ "," ... "," TYPEVARₙ ")"
-```
-
-The set of base types can be extended thanks to the usual ML type
-declarations such as algebraic datatypes and records.
-
-Built-in types include:
-- `int`, machine integers (size not specified, in practice inherited from OCaml)
-- `string`, mutable strings
-- `'a array`, mutable arrays
-- `exn`, exceptions
-- `constr`, kernel-side terms
-- `pattern`, term patterns
-- `ident`, well-formed identifiers
-
-## Type declarations
-
-One can define new types by the following commands.
-
-```
-VERNAC ::=
-| "Ltac2" "Type" TYPEPARAMS LIDENT
-| "Ltac2" "Type" RECFLAG TYPEPARAMS LIDENT ":=" TYPEDEF
-
-RECFLAG := ( "rec" )
-```
-
-The first command defines an abstract type. It has no use for the end user and
-is dedicated to types representing data coming from the OCaml world.
-
-The second command defines a type with a manifest. There are four possible
-kinds of such definitions: alias, variant, record and open variant types.
-
-```
-TYPEDEF :=
-| TYPE
-| "[" CONSTRUCTORDEF₀ "|" ... "|" CONSTRUCTORDEFₙ "]"
-| "{" FIELDDEF₀ ";" ... ";" FIELDDEFₙ "}"
-| "[" ".." "]"
-
-CONSTRUCTORDEF :=
-| IDENT ( "(" TYPE₀ "," ... "," TYPE₀ ")" )
-
-FIELDDEF :=
-| MUTFLAG IDENT ":" TYPE
-
-MUTFLAG := ( "mutable" )
-```
-
-Aliases are just a name for a given type expression and are transparently
-unfoldable to it. They cannot be recursive.
-
-Variants are sum types defined by constructors and eliminated by
-pattern-matching. They can be recursive, but the `RECFLAG` must be explicitly
-set. Pattern-maching must be exhaustive.
-
-Records are product types with named fields and eliminated by projection.
-Likewise they can be recursive if the `RECFLAG` is set.
-
-Open variants are a special kind of variant types whose constructors are not
-statically defined, but can instead be extended dynamically. A typical example
-is the standard `exn` type. Pattern-matching must always include a catch-all
-clause. They can be extended by the following command.
-
-```
-VERNAC ::=
-| "Ltac2" "Type" TYPEPARAMS QUALID ":=" "[" CONSTRUCTORDEF "]"
-```
-
-## Term Syntax
-
-The syntax of the functional fragment is very close to the one of Ltac1, except
-that it adds a true pattern-matching feature, as well as a few standard
-constructions from ML.
-
-```
-VAR := LIDENT
-
-QUALID := ( MODPATH "." )* LIDENT
-
-CONSTRUCTOR := UIDENT
-
-TERM :=
-| QUALID
-| CONSTRUCTOR TERM₀ ... TERMₙ
-| TERM TERM₀ ... TERMₙ
-| "fun" VAR "=>" TERM
-| "let" VAR ":=" TERM "in" TERM
-| "let" "rec" VAR ":=" TERM "in" TERM
-| "match" TERM "with" BRANCH* "end"
-| INT
-| STRING
-| "[|" TERM₀ ";" ... ";" TERMₙ "|]"
-| "(" TERM₀ "," ... "," TERMₙ ")"
-| "{" FIELD+ "}"
-| TERM "." "(" QUALID ")"
-| TERM₁ "." "(" QUALID ")" ":=" TERM₂
-| "["; TERM₀ ";" ... ";" TERMₙ "]"
-| TERM₁ "::" TERM₂
-| ...
-
-BRANCH :=
-| PATTERN "=>" TERM
-
-PATTERN :=
-| VAR
-| "_"
-| "(" PATTERN₀ "," ... "," PATTERNₙ ")"
-| CONSTRUCTOR PATTERN₀ ... PATTERNₙ
-| "[" "]"
-| PATTERN₁ "::" PATTERN₂
-
-FIELD :=
-| QUALID ":=" TERM
-
-```
-
-In practice, there is some additional syntactic sugar that allows e.g. to
-bind a variable and match on it at the same time, in the usual ML style.
-
-There is a dedicated syntax for list and array litterals.
-
-Limitations: for now, deep pattern matching is not implemented yet.
-
-## Ltac Definitions
-
-One can define a new global Ltac2 value using the following syntax.
-```
-VERNAC ::=
-| "Ltac2" MUTFLAG RECFLAG LIDENT ":=" TERM
-```
-
-For semantic reasons, the body of the Ltac2 definition must be a syntactical
-value, i.e. a function, a constant or a pure constructor recursively applied to
-values.
-
-If the `RECFLAG` is set, the tactic is expanded into a recursive binding.
-
-If the `MUTFLAG` is set, the definition can be redefined at a later stage. This
-can be performed through the following command.
-
-```
-VERNAC ::=
-| "Ltac2" "Set" QUALID ":=" TERM
-```
-
-Mutable definitions act like dynamic binding, i.e. at runtime, the last defined
-value for this entry is chosen. This is useful for global flags and the like.
-
-## Reduction
-
-We use the usual ML call-by-value reduction, with an otherwise unspecified
-evaluation order. This is a design choice making it compatible with OCaml,
-if ever we implement native compilation. The expected equations are as follows.
-```
-(fun x => t) V ≡ t{x := V} (βv)
-
-let x := V in t ≡ t{x := V} (let)
-
-match C V₀ ... Vₙ with ... | C x₀ ... xₙ  => t | ... end ≡ t {xᵢ := Vᵢ} (ι)
-
-(t any term, V values, C constructor)
-```
-
-Note that call-by-value reduction is already a departure from Ltac1 which uses
-heuristics to decide when evaluating an expression. For instance, the following
-expressions do not evaluate the same way in Ltac1.
-
-```
-foo (idtac; let x := 0 in bar)
-
-foo (let x := 0 in bar)
-```
-
-Instead of relying on the `idtac` hack, we would now require an explicit thunk
-not to compute the argument, and `foo` would have e.g. type
-`(unit -> unit) -> unit`.
-
-```
-foo (fun () => let x := 0 in bar)
-```
-
-## Typing
-
-Typing is strict and follows Hindley-Milner system. We will not implement the
-current hackish subtyping semantics, and one will have to resort to conversion
-functions. See notations though to make things more palatable. 
-
-In this setting, all usual argument-free tactics have type `unit -> unit`, but
-one can return as well a value of type `t` thanks to terms of type `unit -> t`,
-or take additional arguments.
-
-## Effects
-
-Regarding effects, nothing involved here, except that instead of using the
-standard IO monad as the ambient effectful world, Ltac2 is going to use the
-tactic monad.
-
-Note that the order of evaluation of application is *not* specified and is
-implementation-dependent, as in OCaml.
-
-We recall that the `Proofview.tactic` monad is essentially a IO monad together
-with backtracking state representing the proof state.
-
-Intuitively a thunk of type `unit -> 'a` can do the following:
-- It can perform non-backtracking IO like printing and setting mutable variables
-- It can fail in a non-recoverable way
-- It can use first-class backtrack. The proper way to figure that is that we
-  morally have the following isomorphism:
-  `(unit -> 'a) ~ (unit -> exn + ('a * (exn -> 'a)))` i.e. thunks can produce a
-  lazy list of results where each tail is waiting for a continuation exception.
-- It can access a backtracking proof state, made out amongst other things of
-  the current evar assignation and the list of goals under focus.
-
-We describe more thoroughly the various effects existing in Ltac2 hereafter.
-
-### Standard IO
-
-The Ltac2 language features non-backtracking IO, notably mutable data and
-printing operations.
-
-Mutable fields of records can be modified using the set syntax. Likewise,
-built-in types like `string` and `array` feature imperative assignment. See
-modules `String` and `Array` respectively.
-
-A few printing primitives are provided in the `Message` module, allowing to
-display information to the user.
-
-### Fatal errors
-
-The Ltac2 language provides non-backtracking exceptions through the
-following primitive in module `Control`.
-
-```
-val throw : exn -> 'a
-```
-
-Contrarily to backtracking exceptions from the next section, this kind of error
-is never caught by backtracking primitives, that is, throwing an exception
-destroys the stack. This is materialized by the following equation, where `E`
-is an evaluation context.
-
-```
-E[throw e] ≡ throw e
-
-(e value)
-```
-
-There is currently no way to catch such an exception and it is a design choice.
-There might be at some future point a way to catch it in a brutal way,
-destroying all backtrack and return values.
-
-### Backtrack
-
-In Ltac2, we have the following backtracking primitives, defined in the
-`Control` module.
-
-```
-Ltac2 Type 'a result := [ Val ('a) | Err (exn) ].
-
-val zero : exn -> 'a
-val plus : (unit -> 'a) -> (exn -> 'a) -> 'a
-val case : (unit -> 'a) -> ('a * (exn -> 'a)) result
-```
-
-If one sees thunks as lazy lists, then `zero` is the empty list and `plus` is
-list concatenation, while `case` is pattern-matching.
-
-The backtracking is first-class, i.e. one can write
-`plus (fun () => "x") (fun _ => "y") : string` producing a backtracking string.
-
-These operations are expected to satisfy a few equations, most notably that they
-form a monoid compatible with sequentialization.
-
-```
-plus t zero ≡ t ()
-plus (fun () => zero e) f ≡ f e
-plus (plus t f) g ≡ plus t (fun e => plus (f e) g)
-
-case (fun () => zero e) ≡ Err e
-case (fun () => plus (fun () => t) f) ≡ Val t f
-
-let x := zero e in u ≡ zero e
-let x := plus t f in u ≡ plus (fun () => let x := t in u) (fun e => let x := f e in u)
-
-(t, u, f, g, e values)
-```
-
-### Goals
-
-A goal is given by the data of its conclusion and hypotheses, i.e. it can be
-represented as `[Γ ⊢ A]`.
-
-The tactic monad naturally operates over the whole proofview, which may
-represent several goals, including none. Thus, there is no such thing as
-*the current goal*. Goals are naturally ordered, though.
-
-It is natural to do the same in Ltac2, but we must provide a way to get access
-to a given goal. This is the role of the `enter` primitive, that applies a
-tactic to each currently focused goal in turn.
-
-```
-val enter : (unit -> unit) -> unit
-```
-
-It is guaranteed that when evaluating `enter f`, `f` is called with exactly one
-goal under focus. Note that `f` may be called several times, or never, depending
-on the number of goals under focus before the call to `enter`.
-
-Accessing the goal data is then implicit in the Ltac2 primitives, and may panic
-if the invariants are not respected. The two essential functions for observing
-goals are given below.
-
-```
-val hyp : ident -> constr
-val goal : unit -> constr
-```
-
-The two above functions panic if there is not exactly one goal under focus.
-In addition, `hyp` may also fail if there is no hypothesis with the
-corresponding name.
-
-# Meta-programming
-
-## Overview
-
-One of the horrendous implementation issues of Ltac is the fact that it is
-never clear whether an object refers to the object world or the meta-world.
-This is an incredible source of slowness, as the interpretation must be
-aware of bound variables and must use heuristics to decide whether a variable
-is a proper one or referring to something in the Ltac context.
-
-Likewise, in Ltac1, constr parsing is implicit, so that `foo 0` is
-not `foo` applied to the Ltac integer expression `0` (Ltac does have a
-non-first-class notion of integers), but rather the Coq term `Datatypes.O`.
-
-We should stop doing that! We need to mark when quoting and unquoting, although
-we need to do that in a short and elegant way so as not to be too cumbersome
-to the user.
-
-## Generic Syntax for Quotations
-
-In general, quotations can be introduced in term by the following syntax, where
-`QUOTENTRY` is some parsing entry.
-```
-TERM ::=
-| QUOTNAME ":" "(" QUOTENTRY ")"
-
-QUOTNAME := IDENT
-```
-
-### Built-in quotations
-
-The current implementation recognizes the following built-in quotations:
-- "ident", which parses identifiers (type `Init.ident`).
-- "constr", which parses Coq terms and produces an-evar free term at runtime
-  (type `Init.constr`).
-- "open_constr", which parses Coq terms and produces a term potentially with
-  holes at runtime (type `Init.constr` as well).
-- "pattern", which parses Coq patterns and produces a pattern used for term
-  matching (type `Init.pattern`).
-- "reference", which parses either a `QUALID` or `"&" IDENT`. Qualified names
-  are globalized at internalization into the corresponding global reference,
-  while `&id` is turned into `Std.VarRef id`. This produces at runtime a
-  `Std.reference`.
-
-The following syntactic sugar is provided for two common cases.
-- `@id` is the same as ident:(id)
-- `'t` is the same as open_constr:(t)
-
-### Strict vs. non-strict mode
-
-Depending on the context, quotations producing terms (i.e. `constr` or
-`open_constr`) are not internalized in the same way. There are two possible
-modes, respectively called the *strict* and the *non-strict* mode.
-
-- In strict mode, all simple identifiers appearing in a term quotation are
-required to be resolvable statically. That is, they must be the short name of
-a declaration which is defined globally, excluding section variables and
-hypotheses. If this doesn't hold, internalization will fail. To work around
-this error, one has to specifically use the `&` notation.
-- In non-strict mode, any simple identifier appearing in a term quotation which
-is not bound in the global context is turned into a dynamic reference to a
-hypothesis. That is to say, internalization will succeed, but the evaluation
-of the term at runtime will fail if there is no such variable in the dynamic
-context.
-
-Strict mode is enforced by default, e.g. for all Ltac2 definitions. Non-strict
-mode is only set when evaluating Ltac2 snippets in interactive proof mode. The
-rationale is that it is cumbersome to explicitly add `&` interactively, while it
-is expected that global tactics enforce more invariants on their code.
-
-## Term Antiquotations
-
-### Syntax
-
-One can also insert Ltac2 code into Coq term, similarly to what was possible in
-Ltac1.
-
-```
-COQCONSTR ::=
-| "ltac2" ":" "(" TERM ")"
-```
-
-Antiquoted terms are expected to have type `unit`, as they are only evaluated
-for their side-effects.
-
-### Semantics
-
-Interpretation of a quoted Coq term is done in two phases, internalization and
-evaluation.
-
-- Internalization is part of the static semantics, i.e. it is done at Ltac2
-  typing time.
-- Evaluation is part of the dynamic semantics, i.e. it is done when
-  a term gets effectively computed by Ltac2.
-
-Remark that typing of Coq terms is a *dynamic* process occuring at Ltac2
-evaluation time, and not at Ltac2 typing time.
-
-#### Static semantics
-
-During internalization, Coq variables are resolved and antiquotations are
-type-checked as Ltac2 terms, effectively producing a `glob_constr` in Coq
-implementation terminology. Note that although it went through the
-type-checking of **Ltac2**, the resulting term has not been fully computed and
-is potentially ill-typed as a runtime **Coq** term.
-
-```
-Ltac2 Definition myconstr () := constr:(nat -> 0).
-// Valid with type `unit -> constr`, but will fail at runtime.
-```
-
-Term antiquotations are type-checked in the enclosing Ltac2 typing context
-of the corresponding term expression. For instance, the following will
-type-check.
-
-```
-let x := '0 in constr:(1 + ltac2:(exact x))
-// type constr
-```
-
-Beware that the typing environment of typing of antiquotations is **not**
-expanded by the Coq binders from the term. Namely, it means that the following
-Ltac2 expression will **not** type-check.
-```
-constr:(fun x : nat => ltac2:(exact x))
-// Error: Unbound variable 'x'
-```
-
-There is a simple reason for that, which is that the following expression would
-not make sense in general.
-```
-constr:(fun x : nat => ltac2:(clear @x; exact x))
-```
-Indeed, a hypothesis can suddenly disappear from the runtime context if some
-other tactic pulls the rug from under you.
-
-Rather, the tactic writer has to resort to the **dynamic** goal environment,
-and must write instead explicitly that she is accessing a hypothesis, typically
-as follows.
-```
-constr:(fun x : nat => ltac2:(exact (hyp @x)))
-```
-
-This pattern is so common that we provide dedicated Ltac2 and Coq term notations
-for it.
-
-- `&x` as an Ltac2 expression expands to `hyp @x`.
-- `&x` as a Coq constr expression expands to
-  `ltac2:(Control.refine (fun () => hyp @x))`.
-
-#### Dynamic semantics
-
-During evaluation, a quoted term is fully evaluated to a kernel term, and is
-in particular type-checked in the current environment.
-
-Evaluation of a quoted term goes as follows.
-- The quoted term is first evaluated by the pretyper.
-- Antiquotations are then evaluated in a context where there is exactly one goal
-under focus, with the hypotheses coming from the current environment extended
-with the bound variables of the term, and the resulting term is fed into the
-quoted term.
-
-Relative orders of evaluation of antiquotations and quoted term are not
-specified.
-
-For instance, in the following example, `tac` will be evaluated in a context
-with exactly one goal under focus, whose last hypothesis is `H : nat`. The
-whole expression will thus evaluate to the term `fun H : nat => nat`.
-```
-let tac () := hyp @H in constr:(fun H : nat => ltac2:(tac ()))
-```
-
-Many standard tactics perform type-checking of their argument before going
-further. It is your duty to ensure that terms are well-typed when calling
-such tactics. Failure to do so will result in non-recoverable exceptions.
-
-## Trivial Term Antiquotations
-
-It is possible to refer to a variable of type `constr` in the Ltac2 environment
-through a specific syntax consistent with the antiquotations presented in
-the notation section.
-
-```
-COQCONSTR ::=
-| "$" LIDENT
-```
-
-In a Coq term, writing `$x` is semantically equivalent to
-`ltac2:(Control.refine (fun () => x))`, up to re-typechecking. It allows to
-insert in a concise way an Ltac2 variable of type `constr` into a Coq term.
-
-## Match over terms
-
-Ltac2 features a construction similar to Ltac1 `match` over terms, although
-in a less hard-wired way.
-
-```
-TERM ::=
-| "match!" TERM "with" CONSTR-MATCHING* "end"
-| "lazy_match!" TERM "with" CONSTR-MATCHING* "end"
-| "multi_match!" TERM "with" CONSTR-MATCHING*"end"
-
-CONSTR-MATCHING :=
-| "|" CONSTR-PATTERN "=>" TERM
-
-CONSTR-PATTERN :=
-| CONSTR
-| "context" LIDENT? "[" CONSTR "]"
-```
-
-This construction is not primitive and is desugared at parsing time into
-calls to term matching functions from the `Pattern` module. Internally, it is
-implemented thanks to a specific scope accepting the `CONSTR-MATCHING` syntax.
-
-Variables from the `CONSTR-PATTERN` are statically bound in the body of the branch, to
-values of type `constr` for the variables from the `CONSTR` pattern and to a
-value of type `Pattern.context` for the variable `LIDENT`.
-
-Note that contrarily to Ltac, only lowercase identifiers are valid as Ltac2
-bindings, so that there will be a syntax error if one of the bound variables
-starts with an uppercase character.
-
-The semantics of this construction is otherwise the same as the corresponding
-one from Ltac1, except that it requires the goal to be focused.
-
-## Match over goals
-
-Similarly, there is a way to match over goals in an elegant way, which is
-just a notation desugared at parsing time.
-
-```
-TERM ::=
-| "match!" MATCH-ORDER? "goal" "with" GOAL-MATCHING* "end"
-| "lazy_match!" MATCH-ORDER? "goal" "with" GOAL-MATCHING* "end"
-| "multi_match!" MATCH-ORDER? "goal" "with" GOAL-MATCHING*"end"
-
-GOAL-MATCHING :=
-| "|" "[" HYP-MATCHING* "|-" CONSTR-PATTERN "]" "=>" TERM
-
-HYP-MATCHING :=
-| LIDENT ":" CONSTR-PATTERN
-
-MATCH-ORDER :=
-| "reverse"
-```
-
-Variables from `HYP-MATCHING` and `CONSTR-PATTERN` are bound in the body of the
-branch. Their types are:
-- `constr` for pattern variables appearing in a `CONSTR`
-- `Pattern.context` for variables binding a context
-- `ident` for variables binding a hypothesis name.
-
-The same identifier caveat as in the case of matching over constr applies, and
-this features has the same semantics as in Ltac1. In particular, a `reverse`
-flag can be specified to match hypotheses from the more recently introduced to
-the least recently introduced one.
-
-# Notations
-
-Notations are the crux of the usability of Ltac1. We should be able to recover
-a feeling similar to the old implementation by using and abusing notations.
-
-## Scopes
-
-A scope is a name given to a grammar entry used to produce some Ltac2 expression
-at parsing time. Scopes are described using a form of S-expression.
-
-```
-SCOPE :=
-| STRING
-| INT
-| LIDENT ( "(" SCOPE₀ "," ... "," SCOPEₙ ")" )
-```
-
-A few scopes contain antiquotation features. For sake of uniformity, all
-antiquotations are introduced by the syntax `"$" VAR`.
-
-The following scopes are built-in.
-- constr:
-  + parses `c = COQCONSTR` and produces `constr:(c)`
-- ident:
-  + parses `id = IDENT` and produces `ident:(id)`
-  + parses `"$" (x = IDENT)` and produces the variable `x`
-- list0(*scope*):
-  + if *scope* parses `ENTRY`, parses ̀`(x₀, ..., xₙ = ENTRY*)` and produces
-    `[x₀; ...; xₙ]`.
-- list0(*scope*, sep = STRING):
-  + if *scope* parses `ENTRY`, parses `(x₀ = ENTRY, "sep", ..., "sep", xₙ = ENTRY)`
-    and produces `[x₀; ...; xₙ]`.
-- list1: same as list0 (with or without separator) but parses `ENTRY+` instead
-  of `ENTRY*`.
-- opt(*scope*)
-  + if *scope* parses `ENTRY`, parses `ENTRY?` and produces either `None` or
-    `Some x` where `x` is the parsed expression.
-- self:
-  + parses a Ltac2 expression at the current level and return it as is.
-- next:
-  + parses a Ltac2 expression at the next level and return it as is.
-- tactic(n = INT):
-  + parses a Ltac2 expression at the provided level *n* and return it as is.
-- thunk(*scope*):
-  + parses the same as *scope*, and if *e* is the parsed expression, returns
-  `fun () => e`.
-- STRING:
-  + parses the corresponding string as a CAMLP5 IDENT and returns `()`.
-- keyword(s = STRING):
-  + parses the string *s* as a keyword and returns `()`.
-- terminal(s = STRING):
-  + parses the string *s* as a keyword, if it is already a
-    keyword, otherwise as an IDENT. Returns `()`.
-- seq(*scope₁*, ..., *scopeₙ*):
-  + parses *scope₁*, ..., *scopeₙ* in this order, and produces a tuple made
-    out of the parsed values in the same order. As an optimization, all
-    subscopes of the form STRING are left out of the returned tuple, instead
-    of returning a useless unit value. It is forbidden for the various
-    subscopes to refer to the global entry using self of next.
-
-A few other specific scopes exist to handle Ltac1-like syntax, but their use is
-discouraged and they are thus not documented.
-
-For now there is no way to declare new scopes from Ltac2 side, but this is
-planned.
-
-## Notations
-
-The Ltac2 parser can be extended by syntactic notations.
-```
-VERNAC ::=
-| "Ltac2" "Notation" TOKEN+ LEVEL? ":=" TERM
-
-LEVEL := ":" INT
-
-TOKEN :=
-| VAR "(" SCOPE ")"
-| STRING
-```
-
-A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded
-to the provided body where every token from the notation is let-bound to the
-corresponding generated expression.
-
-For instance, assume we perform:
-```
-Ltac2 Notation "foo" c(thunk(constr)) ids(list0(ident)) := Bar.f c ids.
-```
-Then the following expression
-```
-let y := @X in foo (nat -> nat) x $y
-```
-will expand at parsing time to
-```
-let y := @X in
-let c := fun () => constr:(nat -> nat) with ids := [@x; y] in Bar.f c ids
-```
-
-Beware that the order of evaluation of multiple let-bindings is not specified,
-so that you may have to resort to thunking to ensure that side-effects are
-performed at the right time.
-
-## Abbreviations
-
-There exists a special kind of notations, called abbreviations, that is designed
-so that it does not add any parsing rules. It is similar in spirit to Coq
-abbreviations, insofar as its main purpose is to give an absolute name to a
-piece of pure syntax, which can be transparently referred by this name as if it
-were a proper definition. Abbreviations are introduced by the following
-syntax.
-
-```
-VERNAC ::=
-| "Ltac2" "Notation" IDENT ":=" TERM
-```
-
-The abbreviation can then be manipulated just as a normal Ltac2 definition,
-except that it is expanded at internalization time into the given expression.
-Furthermore, in order to make this kind of construction useful in practice in
-an effectful language such as Ltac2, any syntactic argument to an abbreviation
-is thunked on-the-fly during its expansion.
-
-For instance, suppose that we define the following.
-```
-Ltac2 Notation foo := fun x => x ().
-```
-Then we have the following expansion at internalization time.
-```
-foo 0 ↦ (fun x => x ()) (fun _ => 0)
-```
-
-Note that abbreviations are not typechecked at all, and may result in typing
-errors after expansion.
-
-# Evaluation
-
-Ltac2 features a toplevel loop that can be used to evaluate expressions.
-
-```
-VERNAC ::=
-| "Ltac2" "Eval" TERM
-```
-
-This command evaluates the term in the current proof if there is one, or in the
-global environment otherwise, and displays the resulting value to the user
-together with its type. This function is pure in the sense that it does not
-modify the state of the proof, and in particular all side-effects are discarded.
-
-# Debug
-
-When the option `Ltac2 Backtrace` is set, toplevel failures will be printed with
-a backtrace.
-
-# Compatibility layer with Ltac1
-
-## Ltac1 from Ltac2
-
-### Simple API
-
-One can call Ltac1 code from Ltac2 by using the `ltac1` quotation. It parses
-a Ltac1 expression, and semantics of this quotation is the evaluation of the
-corresponding code for its side effects. In particular, in cannot return values,
-and the quotation has type `unit`.
-
-Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited
-to the use of standalone function calls.
-
-### Low-level API
-
-There exists a lower-level FFI into Ltac1 that is not recommended for daily use,
-which is available in the `Ltac2.Ltac1` module. This API allows to directly
-manipulate dynamically-typed Ltac1 values, either through the function calls,
-or using the `ltac1val` quotation. The latter parses the same as `ltac1`, but
-has type `Ltac2.Ltac1.t` instead of `unit`, and dynamically behaves as an Ltac1
-thunk, i.e. `ltac1val:(foo)` corresponds to the tactic closure that Ltac1
-would generate from `idtac; foo`.
-
-Due to intricate dynamic semantics, understanding when Ltac1 value quotations
-focus is very hard. This is why some functions return a continuation-passing
-style value, as it can dispatch dynamically between focused and unfocused
-behaviour.
-
-## Ltac2 from Ltac1
-
-Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation
-instead.
-
-Note that the tactic expression is evaluated eagerly, if one wants to use it as
-an argument to a Ltac1 function, she has to resort to the good old
-`idtac; ltac2:(foo)` trick. For instance, the code below will fail immediately
-and won't print anything.
-
-```
-Ltac mytac tac := idtac "wow"; tac.
-
-Goal True.
-Proof.
-mytac ltac2:(fail).
-```
-
-# Transition from Ltac1
-
-Owing to the use of a bunch of notations, the transition shouldn't be
-atrociously horrible and shockingly painful up to the point you want to retire
-in the Ariège mountains, living off the land and insulting careless bypassers in
-proto-georgian.
-
-That said, we do *not* guarantee you it is going to be a blissful walk either.
-Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with Coq
-will help you.
-
-We list the major changes and the transition strategies hereafter.
-
-## Syntax changes
-
-Due to conflicts, a few syntactic rules have changed.
-
-- The dispatch tactical `tac; [foo|bar]` is now written `tac > [foo|bar]`.
-- Levels of a few operators have been revised. Some tacticals now parse as if
-  they were a normal function, i.e. one has to put parentheses around the
-  argument when it is complex, e.g an abstraction. List of affected tacticals:
-  `try`, `repeat`, `do`, `once`, `progress`, `time`, `abstract`.
-- `idtac` is no more. Either use `()` if you expect nothing to happen,
-  `(fun () => ())` if you want a thunk (see next section), or use printing
-  primitives from the `Message` module if you want to display something.
-
-## Tactic delay
-
-Tactics are not magically delayed anymore, neither as functions nor as
-arguments. It is your responsibility to thunk them beforehand and apply them
-at the call site.
-
-A typical example of a delayed function:
-```
-Ltac foo := blah.
-```
-becomes
-```
-Ltac2 foo () := blah.
-```
-
-All subsequent calls to `foo` must be applied to perform the same effect as
-before.
-
-Likewise, for arguments:
-```
-Ltac bar tac := tac; tac; tac.
-```
-becomes
-```
-Ltac2 bar tac := tac (); tac (); tac ().
-```
-
-We recommend the use of syntactic notations to ease the transition. For
-instance, the first example can alternatively written as:
-```
-Ltac2 foo0 () := blah.
-Ltac2 Notation foo := foo0 ().
-```
-
-This allows to keep the subsequent calls to the tactic as-is, as the
-expression `foo` will be implicitly expanded everywhere into `foo0 ()`. Such
-a trick also works for arguments, as arguments of syntactic notations are
-implicitly thunked. The second example could thus be written as follows.
-
-```
-Ltac2 bar0 tac := tac (); tac (); tac ().
-Ltac2 Notation bar := bar0.
-```
-
-## Variable binding
-
-Ltac1 relies on a crazy amount of dynamic trickery to be able to tell apart
-bound variables from terms, hypotheses and whatnot. There is no such thing in
-Ltac2, as variables are recognized statically and other constructions do not
-live in the same syntactic world. Due to the abuse of quotations, it can
-sometimes be complicated to know what a mere identifier represents in a tactic
-expression. We recommend tracking the context and letting the compiler spit
-typing errors to understand what is going on.
-
-We list below the typical changes one has to perform depending on the static
-errors produced by the typechecker.
-
-### In Ltac expressions
-
-- `Unbound value X`, `Unbound constructor X`:
-  * if `X` is meant to be a term from the current stactic environment, replace
-    the problematic use by `'X`.
-  * if `X` is meant to be a hypothesis from the goal context, replace the
-    problematic use by `&X`.
-
-### In quotations
-
-- `The reference X was not found in the current environment`:
-  * if `X` is meant to be a tactic expression bound by a Ltac2 let or function,
-    replace the problematic use by `$X`.
-  * if `X` is meant to be a hypothesis from the goal context, replace the
-    problematic use by `&X`.
-
-## Exception catching
-
-Ltac2 features a proper exception-catching mechanism. For this reason, the
-Ltac1 mechanism relying on `fail` taking integers and tacticals decreasing it
-has been removed. Now exceptions are preserved by all tacticals, and it is
-your duty to catch it and reraise it depending on your use.
-
-# TODO
-
-- Implement deep pattern-matching.
-- Craft an expressive set of primitive functions
-- Implement native compilation to OCaml
diff --git a/vendor/Ltac2/dune b/vendor/Ltac2/dune
deleted file mode 100644
index 5dbc4db66a..0000000000
--- a/vendor/Ltac2/dune
+++ /dev/null
@@ -1,3 +0,0 @@
-(env
- (dev     (flags :standard -rectypes))
- (release (flags :standard -rectypes)))
diff --git a/vendor/Ltac2/dune-project b/vendor/Ltac2/dune-project
deleted file mode 100644
index 8154e999de..0000000000
--- a/vendor/Ltac2/dune-project
+++ /dev/null
@@ -1,3 +0,0 @@
-(lang dune 1.6)
-(using coq 0.1)
-(name ltac2)
diff --git a/vendor/Ltac2/ltac2.opam b/vendor/Ltac2/ltac2.opam
deleted file mode 100644
index 47ceb882b1..0000000000
--- a/vendor/Ltac2/ltac2.opam
+++ /dev/null
@@ -1,18 +0,0 @@
-synopsis:     "A Tactic Language for Coq."
-description:  "A Tactic Language for Coq."
-name:         "coq-ltac2"
-opam-version: "2.0"
-maintainer:   "Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>"
-authors:      "Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>"
-homepage:     "https://github.com/ppedrot/ltac2"
-dev-repo:     "https://github.com/ppedrot/ltac2.git"
-bug-reports:  "https://github.com/ppedrot/ltac2/issues"
-license:      "LGPL 2.1"
-doc:          "https://ppedrot.github.io/ltac2/doc"
-
-depends: [
-  "coq"           {          = "dev"      }
-  "dune"          { build & >= "1.9.0"    }
-]
-
-build: [ "dune" "build" "-p" name "-j" jobs ]
diff --git a/vendor/Ltac2/src/dune b/vendor/Ltac2/src/dune
deleted file mode 100644
index 332f3644b0..0000000000
--- a/vendor/Ltac2/src/dune
+++ /dev/null
@@ -1,11 +0,0 @@
-(library
- (name ltac2_plugin)
- (public_name ltac2.plugin)
- (modules_without_implementation tac2expr tac2qexpr tac2types)
- (flags :standard -warn-error -9-27-50)
- (libraries coq.plugins.firstorder))
-
-(rule
- (targets g_ltac2.ml)
- (deps (:mlg-file g_ltac2.mlg))
- (action (run coqpp %{mlg-file})))
diff --git a/vendor/Ltac2/tests/Makefile b/vendor/Ltac2/tests/Makefile
deleted file mode 100644
index d85ae90dd6..0000000000
--- a/vendor/Ltac2/tests/Makefile
+++ /dev/null
@@ -1,16 +0,0 @@
-ifeq "$(COQBIN)" ""
-  COQBIN=$(dir $(shell which coqc))/
-endif
-
-all: $(patsubst %.v,%.v.log,$(wildcard *.v))
-
-%.v.log: %.v
-	$(COQBIN)/coqc -I ../src -Q ../theories Ltac2 $< > $@
-	if [ $$? = 0 ]; then \
-		echo "    $<... OK"; \
-	else \
-		echo "    $<... FAIL!"; \
-	fi; \
-
-clean:
-	rm -f *.log
diff --git a/vendor/Ltac2/theories/dune b/vendor/Ltac2/theories/dune
deleted file mode 100644
index 1fe3ba28fe..0000000000
--- a/vendor/Ltac2/theories/dune
+++ /dev/null
@@ -1,6 +0,0 @@
-(coqlib
- (name Ltac2) ; This determines the -R flag
- (public_name ltac2.Ltac2)
- (synopsis "Ltac 2 Plugin")
- (libraries ltac2.plugin))
-