Prepare merge into Coq

70 files changed, 0 insertions, 0 deletions

diff --git a/.gitignore b/vendor/Ltac2/.gitignore
index 00e15f8daa..00e15f8daa 100644
--- a/.gitignore
+++ b/vendor/Ltac2/.gitignore
diff --git a/.travis.yml b/vendor/Ltac2/.travis.yml
index 2628abde45..2628abde45 100644
--- a/.travis.yml
+++ b/vendor/Ltac2/.travis.yml
diff --git a/LICENSE b/vendor/Ltac2/LICENSE
index 27950e8d20..27950e8d20 100644
--- a/LICENSE
+++ b/vendor/Ltac2/LICENSE
diff --git a/Makefile b/vendor/Ltac2/Makefile
index e0e197650d..e0e197650d 100644
--- a/Makefile
+++ b/vendor/Ltac2/Makefile
diff --git a/README.md b/vendor/Ltac2/README.md
index d49dd88076..d49dd88076 100644
--- a/README.md
+++ b/vendor/Ltac2/README.md
diff --git a/_CoqProject b/vendor/Ltac2/_CoqProject
index dda5a8001a..dda5a8001a 100644
--- a/_CoqProject
+++ b/vendor/Ltac2/_CoqProject
diff --git a/doc/ltac2.md b/vendor/Ltac2/doc/ltac2.md
index b217cb08e6..b217cb08e6 100644
--- a/doc/ltac2.md
+++ b/vendor/Ltac2/doc/ltac2.md
diff --git a/dune b/vendor/Ltac2/dune
index 5dbc4db66a..5dbc4db66a 100644
--- a/dune
+++ b/vendor/Ltac2/dune
diff --git a/dune-project b/vendor/Ltac2/dune-project
index 8154e999de..8154e999de 100644
--- a/dune-project
+++ b/vendor/Ltac2/dune-project
diff --git a/ltac2.opam b/vendor/Ltac2/ltac2.opam
index 47ceb882b1..47ceb882b1 100644
--- a/ltac2.opam
+++ b/vendor/Ltac2/ltac2.opam
diff --git a/src/dune b/vendor/Ltac2/src/dune
index 332f3644b0..332f3644b0 100644
--- a/src/dune
+++ b/vendor/Ltac2/src/dune
diff --git a/src/g_ltac2.mlg b/vendor/Ltac2/src/g_ltac2.mlg
index 0071dbb088..0071dbb088 100644
--- a/src/g_ltac2.mlg
+++ b/vendor/Ltac2/src/g_ltac2.mlg
diff --git a/src/ltac2_plugin.mlpack b/vendor/Ltac2/src/ltac2_plugin.mlpack
index 2a25e825cb..2a25e825cb 100644
--- a/src/ltac2_plugin.mlpack
+++ b/vendor/Ltac2/src/ltac2_plugin.mlpack
diff --git a/src/tac2core.ml b/vendor/Ltac2/src/tac2core.ml
index d7e7b91ee6..d7e7b91ee6 100644
--- a/src/tac2core.ml
+++ b/vendor/Ltac2/src/tac2core.ml
diff --git a/src/tac2core.mli b/vendor/Ltac2/src/tac2core.mli
index 9fae65bb3e..9fae65bb3e 100644
--- a/src/tac2core.mli
+++ b/vendor/Ltac2/src/tac2core.mli
diff --git a/src/tac2dyn.ml b/vendor/Ltac2/src/tac2dyn.ml
index 896676f08b..896676f08b 100644
--- a/src/tac2dyn.ml
+++ b/vendor/Ltac2/src/tac2dyn.ml
diff --git a/src/tac2dyn.mli b/vendor/Ltac2/src/tac2dyn.mli
index e995296840..e995296840 100644
--- a/src/tac2dyn.mli
+++ b/vendor/Ltac2/src/tac2dyn.mli
diff --git a/src/tac2entries.ml b/vendor/Ltac2/src/tac2entries.ml
index 9fd01426de..9fd01426de 100644
--- a/src/tac2entries.ml
+++ b/vendor/Ltac2/src/tac2entries.ml
diff --git a/src/tac2entries.mli b/vendor/Ltac2/src/tac2entries.mli
index d493192bb3..d493192bb3 100644
--- a/src/tac2entries.mli
+++ b/vendor/Ltac2/src/tac2entries.mli
diff --git a/src/tac2env.ml b/vendor/Ltac2/src/tac2env.ml
index 93ad57e97e..93ad57e97e 100644
--- a/src/tac2env.ml
+++ b/vendor/Ltac2/src/tac2env.ml
diff --git a/src/tac2env.mli b/vendor/Ltac2/src/tac2env.mli
index c7e87c5432..c7e87c5432 100644
--- a/src/tac2env.mli
+++ b/vendor/Ltac2/src/tac2env.mli
diff --git a/src/tac2expr.mli b/vendor/Ltac2/src/tac2expr.mli
index 1069d0bfa3..1069d0bfa3 100644
--- a/src/tac2expr.mli
+++ b/vendor/Ltac2/src/tac2expr.mli
diff --git a/src/tac2extffi.ml b/vendor/Ltac2/src/tac2extffi.ml
index 315c970f9e..315c970f9e 100644
--- a/src/tac2extffi.ml
+++ b/vendor/Ltac2/src/tac2extffi.ml
diff --git a/src/tac2extffi.mli b/vendor/Ltac2/src/tac2extffi.mli
index f5251c3d0d..f5251c3d0d 100644
--- a/src/tac2extffi.mli
+++ b/vendor/Ltac2/src/tac2extffi.mli
diff --git a/src/tac2ffi.ml b/vendor/Ltac2/src/tac2ffi.ml
index e3127ab9df..e3127ab9df 100644
--- a/src/tac2ffi.ml
+++ b/vendor/Ltac2/src/tac2ffi.ml
diff --git a/src/tac2ffi.mli b/vendor/Ltac2/src/tac2ffi.mli
index bfc93d99e6..bfc93d99e6 100644
--- a/src/tac2ffi.mli
+++ b/vendor/Ltac2/src/tac2ffi.mli
diff --git a/src/tac2intern.ml b/vendor/Ltac2/src/tac2intern.ml
index de99fb167f..de99fb167f 100644
--- a/src/tac2intern.ml
+++ b/vendor/Ltac2/src/tac2intern.ml
diff --git a/src/tac2intern.mli b/vendor/Ltac2/src/tac2intern.mli
index d646b5cda5..d646b5cda5 100644
--- a/src/tac2intern.mli
+++ b/vendor/Ltac2/src/tac2intern.mli
diff --git a/src/tac2interp.ml b/vendor/Ltac2/src/tac2interp.ml
index b0f8083aeb..b0f8083aeb 100644
--- a/src/tac2interp.ml
+++ b/vendor/Ltac2/src/tac2interp.ml
diff --git a/src/tac2interp.mli b/vendor/Ltac2/src/tac2interp.mli
index 21fdcd03af..21fdcd03af 100644
--- a/src/tac2interp.mli
+++ b/vendor/Ltac2/src/tac2interp.mli
diff --git a/src/tac2match.ml b/vendor/Ltac2/src/tac2match.ml
index c9e549d47e..c9e549d47e 100644
--- a/src/tac2match.ml
+++ b/vendor/Ltac2/src/tac2match.ml
diff --git a/src/tac2match.mli b/vendor/Ltac2/src/tac2match.mli
index c82c40d238..c82c40d238 100644
--- a/src/tac2match.mli
+++ b/vendor/Ltac2/src/tac2match.mli
diff --git a/src/tac2print.ml b/vendor/Ltac2/src/tac2print.ml
index f4cb290265..f4cb290265 100644
--- a/src/tac2print.ml
+++ b/vendor/Ltac2/src/tac2print.ml
diff --git a/src/tac2print.mli b/vendor/Ltac2/src/tac2print.mli
index 9b9db2937d..9b9db2937d 100644
--- a/src/tac2print.mli
+++ b/vendor/Ltac2/src/tac2print.mli
diff --git a/src/tac2qexpr.mli b/vendor/Ltac2/src/tac2qexpr.mli
index 400ab1a092..400ab1a092 100644
--- a/src/tac2qexpr.mli
+++ b/vendor/Ltac2/src/tac2qexpr.mli
diff --git a/src/tac2quote.ml b/vendor/Ltac2/src/tac2quote.ml
index a98264745e..a98264745e 100644
--- a/src/tac2quote.ml
+++ b/vendor/Ltac2/src/tac2quote.ml
diff --git a/src/tac2quote.mli b/vendor/Ltac2/src/tac2quote.mli
index 1b03dad8ec..1b03dad8ec 100644
--- a/src/tac2quote.mli
+++ b/vendor/Ltac2/src/tac2quote.mli
diff --git a/src/tac2stdlib.ml b/vendor/Ltac2/src/tac2stdlib.ml
index ffef2c05fd..ffef2c05fd 100644
--- a/src/tac2stdlib.ml
+++ b/vendor/Ltac2/src/tac2stdlib.ml
diff --git a/src/tac2stdlib.mli b/vendor/Ltac2/src/tac2stdlib.mli
index 927b57074d..927b57074d 100644
--- a/src/tac2stdlib.mli
+++ b/vendor/Ltac2/src/tac2stdlib.mli
diff --git a/src/tac2tactics.ml b/vendor/Ltac2/src/tac2tactics.ml
index ce37a613b1..ce37a613b1 100644
--- a/src/tac2tactics.ml
+++ b/vendor/Ltac2/src/tac2tactics.ml
diff --git a/src/tac2tactics.mli b/vendor/Ltac2/src/tac2tactics.mli
index 026673acbf..026673acbf 100644
--- a/src/tac2tactics.mli
+++ b/vendor/Ltac2/src/tac2tactics.mli
diff --git a/src/tac2types.mli b/vendor/Ltac2/src/tac2types.mli
index fa31153a27..fa31153a27 100644
--- a/src/tac2types.mli
+++ b/vendor/Ltac2/src/tac2types.mli
diff --git a/tests/Makefile b/vendor/Ltac2/tests/Makefile
index d85ae90dd6..d85ae90dd6 100644
--- a/tests/Makefile
+++ b/vendor/Ltac2/tests/Makefile
diff --git a/tests/compat.v b/vendor/Ltac2/tests/compat.v
index 489fa638e4..489fa638e4 100644
--- a/tests/compat.v
+++ b/vendor/Ltac2/tests/compat.v
diff --git a/tests/errors.v b/vendor/Ltac2/tests/errors.v
index c677f6af5d..c677f6af5d 100644
--- a/tests/errors.v
+++ b/vendor/Ltac2/tests/errors.v
diff --git a/tests/example1.v b/vendor/Ltac2/tests/example1.v
index 023791050f..023791050f 100644
--- a/tests/example1.v
+++ b/vendor/Ltac2/tests/example1.v
diff --git a/tests/example2.v b/vendor/Ltac2/tests/example2.v
index c953d25061..c953d25061 100644
--- a/tests/example2.v
+++ b/vendor/Ltac2/tests/example2.v
diff --git a/tests/matching.v b/vendor/Ltac2/tests/matching.v
index 4338cbd32f..4338cbd32f 100644
--- a/tests/matching.v
+++ b/vendor/Ltac2/tests/matching.v
diff --git a/tests/quot.v b/vendor/Ltac2/tests/quot.v
index 624c4ad0c1..624c4ad0c1 100644
--- a/tests/quot.v
+++ b/vendor/Ltac2/tests/quot.v
diff --git a/tests/rebind.v b/vendor/Ltac2/tests/rebind.v
index e1c20a2059..e1c20a2059 100644
--- a/tests/rebind.v
+++ b/vendor/Ltac2/tests/rebind.v
diff --git a/tests/stuff/ltac2.v b/vendor/Ltac2/tests/stuff/ltac2.v
index 370bc70d15..370bc70d15 100644
--- a/tests/stuff/ltac2.v
+++ b/vendor/Ltac2/tests/stuff/ltac2.v
diff --git a/tests/tacticals.v b/vendor/Ltac2/tests/tacticals.v
index 1a2fbcbb37..1a2fbcbb37 100644
--- a/tests/tacticals.v
+++ b/vendor/Ltac2/tests/tacticals.v
diff --git a/tests/typing.v b/vendor/Ltac2/tests/typing.v
index 9f18292716..9f18292716 100644
--- a/tests/typing.v
+++ b/vendor/Ltac2/tests/typing.v
diff --git a/theories/Array.v b/vendor/Ltac2/theories/Array.v
index 11b64e3515..11b64e3515 100644
--- a/theories/Array.v
+++ b/vendor/Ltac2/theories/Array.v
diff --git a/theories/Char.v b/vendor/Ltac2/theories/Char.v
index 29fef60f2c..29fef60f2c 100644
--- a/theories/Char.v
+++ b/vendor/Ltac2/theories/Char.v
diff --git a/theories/Constr.v b/vendor/Ltac2/theories/Constr.v
index d8d222730e..d8d222730e 100644
--- a/theories/Constr.v
+++ b/vendor/Ltac2/theories/Constr.v
diff --git a/theories/Control.v b/vendor/Ltac2/theories/Control.v
index 071c2ea8ce..071c2ea8ce 100644
--- a/theories/Control.v
+++ b/vendor/Ltac2/theories/Control.v
diff --git a/theories/Env.v b/vendor/Ltac2/theories/Env.v
index c9b250f4ba..c9b250f4ba 100644
--- a/theories/Env.v
+++ b/vendor/Ltac2/theories/Env.v
diff --git a/theories/Fresh.v b/vendor/Ltac2/theories/Fresh.v
index 5e876bb077..5e876bb077 100644
--- a/theories/Fresh.v
+++ b/vendor/Ltac2/theories/Fresh.v
diff --git a/theories/Ident.v b/vendor/Ltac2/theories/Ident.v
index 55456afbe2..55456afbe2 100644
--- a/theories/Ident.v
+++ b/vendor/Ltac2/theories/Ident.v
diff --git a/theories/Init.v b/vendor/Ltac2/theories/Init.v
index 16e7d7a6f9..16e7d7a6f9 100644
--- a/theories/Init.v
+++ b/vendor/Ltac2/theories/Init.v
diff --git a/theories/Int.v b/vendor/Ltac2/theories/Int.v
index 0a90d757b6..0a90d757b6 100644
--- a/theories/Int.v
+++ b/vendor/Ltac2/theories/Int.v
diff --git a/theories/Ltac1.v b/vendor/Ltac2/theories/Ltac1.v
index c4e0b606d0..c4e0b606d0 100644
--- a/theories/Ltac1.v
+++ b/vendor/Ltac2/theories/Ltac1.v
diff --git a/theories/Ltac2.v b/vendor/Ltac2/theories/Ltac2.v
index ac90f63560..ac90f63560 100644
--- a/theories/Ltac2.v
+++ b/vendor/Ltac2/theories/Ltac2.v
diff --git a/theories/Message.v b/vendor/Ltac2/theories/Message.v
index 7bffe0746b..7bffe0746b 100644
--- a/theories/Message.v
+++ b/vendor/Ltac2/theories/Message.v
diff --git a/theories/Notations.v b/vendor/Ltac2/theories/Notations.v
index f4621656d6..f4621656d6 100644
--- a/theories/Notations.v
+++ b/vendor/Ltac2/theories/Notations.v
diff --git a/theories/Pattern.v b/vendor/Ltac2/theories/Pattern.v
index 8d1fb0cd8a..8d1fb0cd8a 100644
--- a/theories/Pattern.v
+++ b/vendor/Ltac2/theories/Pattern.v
diff --git a/theories/Std.v b/vendor/Ltac2/theories/Std.v
index 73b2ba02c4..73b2ba02c4 100644
--- a/theories/Std.v
+++ b/vendor/Ltac2/theories/Std.v
diff --git a/theories/String.v b/vendor/Ltac2/theories/String.v
index 99e1dab76b..99e1dab76b 100644
--- a/theories/String.v
+++ b/vendor/Ltac2/theories/String.v
diff --git a/theories/dune b/vendor/Ltac2/theories/dune
index 1fe3ba28fe..1fe3ba28fe 100644
--- a/theories/dune
+++ b/vendor/Ltac2/theories/dune