Turning the ltac2 subfolder into a standalone plugin.

28 files changed, 629 insertions, 110 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000000..ffdea1320c
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,14 @@
+Makefile.coq
+Makefile.coq.conf
+*.glob
+*.d
+*.d.raw
+*.vio
+*.vo
+*.cm*
+*.annot
+*.spit
+*.spot
+*.o
+*.a
+*.aux
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000000..27950e8d20
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,458 @@
+		  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/Makefile b/Makefile
new file mode 100644
index 0000000000..cfdeeba747
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,12 @@
+all: Makefile.coq
+	$(MAKE) -f Makefile.coq
+
+install: all
+	$(MAKE) -f Makefile.coq install
+
+clean: Makefile.coq
+	$(MAKE) -f Makefile.coq clean
+	rm -f Makefile.coq
+
+Makefile.coq: _CoqProject
+	$(COQBIN)/coq_makefile -f _CoqProject -o Makefile.coq
diff --git a/README.md b/README.md
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/README.md
diff --git a/_CoqProject b/_CoqProject
new file mode 100644
index 0000000000..90338abbfb
--- /dev/null
+++ b/_CoqProject
@@ -0,0 +1,28 @@
+-R theories/ Ltac2
+-I src/
+-bypass-API
+
+src/tac2expr.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/tac2core.ml
+src/tac2core.mli
+src/g_ltac2.ml4
+src/ltac2_plugin.mlpack
+
+theories/Init.v
+theories/Int.v
+theories/String.v
+theories/Array.v
+theories/Control.v
+theories/Message.v
+theories/Constr.v
+theories/Ltac2.v
diff --git a/g_ltac2.ml4 b/src/g_ltac2.ml4
index 51919addf2..36057b3a67 100644
--- a/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -36,9 +36,9 @@ GEXTEND Gram
       | id = Prim.qualid -> CPatRef (!@loc, RelId id, []) ]
     | "0"
       [ "_" -> CPatAny (!@loc)
-      | "()" -> CPatTup (!@loc, [])
+      | "()" -> CPatTup (Loc.tag ~loc:!@loc [])
       | id = Prim.qualid -> CPatRef (!@loc, RelId id, [])
-      | "("; pl = LIST0 tac2pat LEVEL "1" SEP ","; ")" -> CPatTup (!@loc, pl) ]
+      | "("; pl = LIST0 tac2pat LEVEL "1" SEP ","; ")" -> CPatTup (Loc.tag ~loc:!@loc pl) ]
     ]
   ;
   tac2expr:
@@ -56,13 +56,13 @@ GEXTEND Gram
       [ e = tac2expr; el = LIST1 tac2expr LEVEL "0" -> CTacApp (!@loc, e, el)
       | e = SELF; ".("; qid = Prim.qualid; ")" -> CTacPrj (!@loc, e, RelId qid)
       | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "1" -> CTacSet (!@loc, e, RelId qid, r)
-      | e0 = tac2expr; ","; el = LIST1 tac2expr LEVEL "1" SEP "," -> CTacTup (!@loc, e0 :: el) ]
+      | e0 = tac2expr; ","; el = LIST1 tac2expr LEVEL "1" SEP "," -> CTacTup (Loc.tag ~loc:!@loc (e0 :: el)) ]
     | "0"
       [ "("; a = tac2expr LEVEL "5"; ")" -> a
       | "("; a = tac2expr; ":"; t = tac2type; ")" -> CTacCnv (!@loc, a, t)
-      | "()" -> CTacTup (!@loc, [])
-      | "("; ")" -> CTacTup (!@loc, [])
-      | "["; a = LIST0 tac2expr LEVEL "1" SEP ";"; "]" -> CTacLst (!@loc, a)
+      | "()" -> CTacTup (Loc.tag ~loc:!@loc [])
+      | "("; ")" -> CTacTup (Loc.tag ~loc:!@loc [])
+      | "["; a = LIST0 tac2expr LEVEL "1" SEP ";"; "]" -> CTacLst (Loc.tag ~loc:!@loc a)
       | "{"; a = tac2rec_fieldexprs; "}" -> CTacRec (!@loc, a)
       | a = tactic_atom -> a ]
     ]
@@ -84,8 +84,8 @@ GEXTEND Gram
     [ [ "'"; id = Prim.ident -> id ] ]
   ;
   tactic_atom:
-    [ [ n = Prim.integer -> CTacAtm (!@loc, AtmInt n)
-      | s = Prim.string -> CTacAtm (!@loc, AtmStr s)
+    [ [ n = Prim.integer -> CTacAtm (Loc.tag ~loc:!@loc (AtmInt n))
+      | s = Prim.string -> CTacAtm (Loc.tag ~loc:!@loc (AtmStr s))
       | id = Prim.qualid -> CTacRef (RelId id)
       | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_constr !@loc c
       | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_open_constr !@loc c
@@ -107,18 +107,18 @@ GEXTEND Gram
       [ t = SELF; qid = Prim.qualid -> CTypRef (!@loc, RelId qid, [t]) ]
     | "0"
       [ "("; t = tac2type LEVEL "5"; ")"  -> t
-      | id = typ_param -> CTypVar (!@loc, Name id)
-      | "_" -> CTypVar (!@loc, Anonymous)
+      | id = typ_param -> CTypVar (Loc.tag ~loc:!@loc (Name id))
+      | "_" -> CTypVar (Loc.tag ~loc:!@loc Anonymous)
       | qid = Prim.qualid -> CTypRef (!@loc, RelId qid, [])
       | "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid ->
         CTypRef (!@loc, RelId qid, p) ]
     ];
   locident:
-    [ [ id = Prim.ident -> (!@loc, id) ] ]
+    [ [ id = Prim.ident -> Loc.tag ~loc:!@loc id ] ]
   ;
   binder:
-    [ [ "_" -> (!@loc, Anonymous)
-      | l = Prim.ident -> (!@loc, Name l) ] ]
+    [ [ "_" -> Loc.tag ~loc:!@loc Anonymous
+      | l = Prim.ident -> Loc.tag ~loc:!@loc (Name l) ] ]
   ;
   input_fun:
     [ [ b = binder -> (b, None)
@@ -169,8 +169,8 @@ GEXTEND Gram
   ;
   tac2typ_prm:
     [ [ -> []
-      | id = typ_param -> [!@loc, id]
-      | "("; ids = LIST1 [ id = typ_param -> (!@loc, id) ] SEP "," ;")" -> ids
+      | id = typ_param -> [Loc.tag ~loc:!@loc id]
+      | "("; ids = LIST1 [ id = typ_param -> Loc.tag ~loc:!@loc id ] SEP "," ;")" -> ids
     ] ]
   ;
   tac2typ_def:
@@ -195,13 +195,13 @@ GEXTEND Gram
     ] ]
   ;
   syn_node:
-    [ [ "_" -> (!@loc, None)
-      | id = Prim.ident -> (!@loc, Some id)
+    [ [ "_" -> Loc.tag ~loc:!@loc None
+      | id = Prim.ident -> Loc.tag ~loc:!@loc (Some id)
     ] ]
   ;
   sexpr:
-    [ [ s = Prim.string -> SexprStr (!@loc, s)
-      | n = Prim.integer -> SexprInt (!@loc, n)
+    [ [ s = Prim.string -> SexprStr (Loc.tag ~loc:!@loc s)
+      | n = Prim.integer -> SexprInt (Loc.tag ~loc:!@loc n)
       | id = syn_node -> SexprRec (!@loc, id, [])
       | id = syn_node; "("; tok = LIST1 sexpr SEP "," ; ")" ->
         SexprRec (!@loc, id, tok)
@@ -224,7 +224,7 @@ GEXTEND Gram
   Pcoq.Constr.operconstr: LEVEL "0"
     [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
           let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
-          CHole (!@loc, None, IntroAnonymous, Some arg) ] ]
+          CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg)) ] ]
   ;
 END
 
diff --git a/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack
index 3d87a8cddb..3d87a8cddb 100644
--- a/ltac2_plugin.mlpack
+++ b/src/ltac2_plugin.mlpack
diff --git a/tac2core.ml b/src/tac2core.ml
index c82893efc2..91a3bfa168 100644
--- a/tac2core.ml
+++ b/src/tac2core.ml
@@ -382,10 +382,10 @@ let prm_new_goal : ml_tactic = function
 (** unit -> constr *)
 let prm_goal : ml_tactic = function
 | [_] ->
-  Proofview.Goal.enter_one { enter = fun gl ->
+  Proofview.Goal.enter_one begin fun gl ->
     let concl = Tacmach.New.pf_nf_concl gl in
     return (Value.of_constr concl)
-  }
+  end
 | _ -> assert false
 
 (** ident -> constr *)
@@ -404,9 +404,9 @@ let prm_hyp : ml_tactic = function
 let prm_refine : ml_tactic = function
 | [c] ->
   let c = thaw c >>= fun c -> Proofview.tclUNIT ((), Value.to_constr c) in
-  Proofview.Goal.nf_enter { enter = fun gl ->
-    Refine.generic_refine ~unsafe:false c gl
-  } >>= fun () -> return v_unit
+  Proofview.Goal.nf_enter begin fun gl ->
+    Refine.generic_refine ~typecheck:true c gl
+  end >>= fun () -> return v_unit
 | _ -> assert false
 
 
@@ -479,10 +479,10 @@ let open_constr_no_classes_flags () =
 
 (** Embed all Ltac2 data into Values *)
 let to_lvar ist =
-  let open Pretyping in
+  let open Glob_ops in
   let map e = Val.Dyn (val_valexpr, e) in
   let lfun = Id.Map.map map ist in
-  { empty_lvar with ltac_genargs = lfun }
+  { empty_lvar with Glob_term.ltac_genargs = lfun }
 
 let interp_constr flags ist (c, _) =
   let open Pretyping in
@@ -541,16 +541,18 @@ let add_scope s f =
 
 let scope_fail () = CErrors.user_err (str "Invalid parsing token")
 
+let dummy_loc = Loc.make_loc (-1, -1)
+
 let rthunk e =
   let loc = Tac2intern.loc_of_tacexpr e in
-  let var = [(loc, Anonymous), Some (CTypRef (loc, AbsKn Core.t_unit, []))] in
+  let var = [Loc.tag ~loc Anonymous, Some (CTypRef (loc, AbsKn Core.t_unit, []))] in
   CTacFun (loc, var, e)
 
 let add_generic_scope s entry arg =
   let parse = function
   | [] ->
     let scope = Extend.Aentry entry in
-    let act x = rthunk (CTacExt (Loc.ghost, in_gen (rawwit arg) x)) in
+    let act x = rthunk (CTacExt (dummy_loc, in_gen (rawwit arg) x)) in
     Tac2entries.ScopeRule (scope, act)
   | _ -> scope_fail ()
   in
@@ -562,7 +564,7 @@ let () = add_scope "list0" begin function
   let scope = Extend.Alist0 scope in
   let act l =
     let l = List.map act l in
-    CTacLst (Loc.ghost, l)
+    CTacLst (None, l)
   in
   Tac2entries.ScopeRule (scope, act)
 | [tok; SexprStr (_, str)] ->
@@ -571,7 +573,7 @@ let () = add_scope "list0" begin function
   let scope = Extend.Alist0sep (scope, sep) in
   let act l =
     let l = List.map act l in
-    CTacLst (Loc.ghost, l)
+    CTacLst (None, l)
   in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
@@ -583,7 +585,7 @@ let () = add_scope "list1" begin function
   let scope = Extend.Alist1 scope in
   let act l =
     let l = List.map act l in
-    CTacLst (Loc.ghost, l)
+    CTacLst (None, l)
   in
   Tac2entries.ScopeRule (scope, act)
 | [tok; SexprStr (_, str)] ->
@@ -592,7 +594,7 @@ let () = add_scope "list1" begin function
   let scope = Extend.Alist1sep (scope, sep) in
   let act l =
     let l = List.map act l in
-    CTacLst (Loc.ghost, l)
+    CTacLst (None, l)
   in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
@@ -606,7 +608,7 @@ let () = add_scope "opt" begin function
   | None ->
     CTacRef (AbsKn (TacConstructor Core.c_none))
   | Some x ->
-    CTacApp (Loc.ghost, CTacRef (AbsKn (TacConstructor Core.c_some)), [act x])
+    CTacApp (dummy_loc, CTacRef (AbsKn (TacConstructor Core.c_some)), [act x])
   in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
diff --git a/tac2core.mli b/src/tac2core.mli
index fc90499ac6..fc90499ac6 100644
--- a/tac2core.mli
+++ b/src/tac2core.mli
diff --git a/tac2entries.ml b/src/tac2entries.ml
index 3959e705ed..46f390a6d4 100644
--- a/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -239,6 +239,8 @@ let inTypExt : typext -> obj =
 
 (** Toplevel entries *)
 
+let dummy_loc = Loc.make_loc (-1, -1)
+
 let register_ltac ?(local = false) isrec tactics =
   if isrec then
     let map (na, e) = (na, None, e) in
@@ -247,7 +249,7 @@ let register_ltac ?(local = false) isrec tactics =
     | Anonymous -> None
     | Name id ->
       let qid = Libnames.qualid_of_ident id in
-      let e = CTacLet (Loc.ghost, true, bindings, CTacRef (RelId (loc, qid))) in
+      let e = CTacLet (dummy_loc, true, bindings, CTacRef (RelId (loc, qid))) in
       let (e, t) = intern e in
       let e = match e with
       | GTacLet (true, _, e) -> assert false
@@ -262,11 +264,11 @@ let register_ltac ?(local = false) isrec tactics =
       let (e, t) = intern e in
       let () =
         if not (is_value e) then
-          user_err ~loc (str "Tactic definition must be a syntactical value")
+          user_err ?loc (str "Tactic definition must be a syntactical value")
       in
       let id = match na with
       | Anonymous ->
-        user_err ~loc (str "Tactic definition must have a name")
+        user_err ?loc (str "Tactic definition must have a name")
       | Name id -> id
       in
       let kn = Lib.make_kn id in
@@ -275,7 +277,7 @@ let register_ltac ?(local = false) isrec tactics =
       in
       let () =
         if exists then
-          user_err ~loc (str "Tactic " ++ Nameops.pr_id id ++ str " already exists")
+          user_err ?loc (str "Tactic " ++ Nameops.pr_id id ++ str " already exists")
       in
       (id, e, t)
     in
@@ -293,27 +295,27 @@ let register_ltac ?(local = false) isrec tactics =
 let qualid_to_ident (loc, qid) =
   let (dp, id) = Libnames.repr_qualid qid in
   if DirPath.is_empty dp then (loc, id)
-  else user_err ~loc (str "Identifier expected")
+  else user_err ?loc (str "Identifier expected")
 
 let register_typedef ?(local = false) isrec types =
   let same_name ((_, id1), _) ((_, id2), _) = Id.equal id1 id2 in
   let () = match List.duplicates same_name types with
   | [] -> ()
   | ((loc, id), _) :: _ ->
-    user_err ~loc (str "Multiple definition of the type name " ++ Id.print id)
+    user_err ?loc (str "Multiple definition of the type name " ++ Id.print id)
   in
   let check ((loc, id), (params, def)) =
     let same_name (_, id1) (_, id2) = Id.equal id1 id2 in
     let () = match List.duplicates same_name params with
     | [] -> ()
     | (loc, id) :: _ ->
-      user_err ~loc (str "The type parameter " ++ Id.print id ++
+      user_err ?loc (str "The type parameter " ++ Id.print id ++
         str " occurs several times")
     in
     match def with
     | CTydDef _ ->
       if isrec then
-        user_err ~loc (str "The type abbreviation " ++ Id.print id ++
+        user_err ?loc (str "The type abbreviation " ++ Id.print id ++
           str " cannot be recursive")
     | CTydAlg cs ->
       let same_name (id1, _) (id2, _) = Id.equal id1 id2 in
@@ -333,7 +335,7 @@ let register_typedef ?(local = false) isrec types =
       ()
     | CTydOpn ->
       if isrec then
-        user_err ~loc (str "The open type declaration " ++ Id.print id ++
+        user_err ?loc (str "The open type declaration " ++ Id.print id ++
           str " cannot be recursive")
   in
   let () = List.iter check types in
@@ -364,10 +366,10 @@ let register_primitive ?(local = false) (loc, id) t ml =
   in
   let arrows = count_arrow (snd t) in
   let () = if Int.equal arrows 0 then
-    user_err ~loc (str "External tactic must have at least one argument") in
+    user_err ?loc (str "External tactic must have at least one argument") in
   let () =
     try let _ = Tac2env.interp_primitive ml in () with Not_found ->
-      user_err ~loc (str "Unregistered primitive " ++
+      user_err ?loc (str "Unregistered primitive " ++
         quote (str ml.mltac_plugin) ++ spc () ++ quote (str ml.mltac_tactic))
   in
   let init i = Id.of_string (Printf.sprintf "x%i" i) in
@@ -386,15 +388,16 @@ let register_open ?(local = false) (loc, qid) (params, def) =
   let kn =
     try Tac2env.locate_type qid
     with Not_found ->
-      user_err ~loc (str "Unbound type " ++ pr_qualid qid)
+      user_err ?loc (str "Unbound type " ++ pr_qualid qid)
   in
   let (tparams, t) = Tac2env.interp_type kn in
   let () = match t with
   | GTydOpn -> ()
   | GTydAlg _ | GTydRec _ | GTydDef _ ->
-    user_err ~loc (str "Type " ++ pr_qualid qid ++ str " is not an open type")
+    user_err ?loc (str "Type " ++ pr_qualid qid ++ str " is not an open type")
   in
   let () =
+    let loc = Option.default dummy_loc loc in
     if not (Int.equal (List.length params) tparams) then
       Tac2intern.error_nparams_mismatch loc (List.length params) tparams
   in
@@ -421,18 +424,18 @@ let register_open ?(local = false) (loc, qid) (params, def) =
     } in
     Lib.add_anonymous_leaf (inTypExt def)
   | CTydRec _ | CTydDef _ ->
-    user_err ~loc (str "Extensions only accept inductive constructors")
+    user_err ?loc (str "Extensions only accept inductive constructors")
 
 let register_type ?local isrec types = match types with
 | [qid, true, def] ->
   let (loc, _) = qid in
-  let () = if isrec then user_err ~loc (str "Extensions cannot be recursive") in
+  let () = if isrec then user_err ?loc (str "Extensions cannot be recursive") in
   register_open ?local qid def
 | _ ->
   let map (qid, redef, def) =
     let (loc, _) = qid in
     let () = if redef then
-      user_err ~loc (str "Types can only be extended one by one")
+      user_err ?loc (str "Types can only be extended one by one")
     in
     (qualid_to_ident qid, def)
   in
@@ -459,8 +462,8 @@ module ParseToken =
 struct
 
 let loc_of_token = function
-| SexprStr (loc, _) -> loc
-| SexprInt (loc, _) -> loc
+| SexprStr (loc, _) -> Option.default dummy_loc loc
+| SexprInt (loc, _) -> Option.default dummy_loc loc
 | SexprRec (loc, _, _) -> loc
 
 let parse_scope = function
@@ -468,7 +471,7 @@ let parse_scope = function
   if Id.Map.mem id !scope_table then
     Id.Map.find id !scope_table toks
   else
-    CErrors.user_err ~loc (str "Unknown scope" ++ spc () ++ Nameops.pr_id id)
+    CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Nameops.pr_id id)
 | tok ->
   let loc = loc_of_token tok in
   CErrors.user_err ~loc (str "Invalid parsing token")
@@ -518,7 +521,7 @@ let perform_notation syn st =
   let mk loc args =
     let map (na, e) =
       let loc = loc_of_tacexpr e in
-      ((loc, na), None, e)
+      (Loc.tag ~loc na, None, e)
     in
     let bnd = List.map map args in
     CTacLet (loc, false, bnd, syn.synext_exp)
@@ -587,7 +590,7 @@ let print_ltac ref =
   let (loc, qid) = qualid_of_reference ref in
   let kn =
     try Tac2env.locate_ltac qid
-    with Not_found -> user_err ~loc (str "Unknown tactic " ++ pr_qualid qid)
+    with Not_found -> user_err ?loc (str "Unknown tactic " ++ pr_qualid qid)
   in
   match kn with
   | TacConstant kn ->
diff --git a/tac2entries.mli b/src/tac2entries.mli
index 71e8150057..71e8150057 100644
--- a/tac2entries.mli
+++ b/src/tac2entries.mli
diff --git a/tac2env.ml b/src/tac2env.ml
index 5ccdd018ee..5ccdd018ee 100644
--- a/tac2env.ml
+++ b/src/tac2env.ml
diff --git a/tac2env.mli b/src/tac2env.mli
index c4b8c1e0ca..c4b8c1e0ca 100644
--- a/tac2env.mli
+++ b/src/tac2env.mli
diff --git a/tac2expr.mli b/src/tac2expr.mli
index acdad9bab4..acdad9bab4 100644
--- a/tac2expr.mli
+++ b/src/tac2expr.mli
diff --git a/tac2intern.ml b/src/tac2intern.ml
index 756bbe3076..b63e6a0cd8 100644
--- a/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -179,22 +179,24 @@ let get_alias (loc, id) env =
       let n = fresh_id env in
       let () = env.env_als := Id.Map.add id n env.env_als.contents in
       n
-    else user_err ~loc (str "Unbound type parameter " ++ Id.print id)
+    else user_err ?loc (str "Unbound type parameter " ++ Id.print id)
 
 let push_name id t env = match id with
 | Anonymous -> env
 | Name id -> { env with env_var = Id.Map.add id t env.env_var }
 
+let dummy_loc = Loc.make_loc (-1, -1)
+
 let loc_of_tacexpr = function
-| CTacAtm (loc, _) -> loc
-| CTacRef (RelId (loc, _)) -> loc
-| CTacRef (AbsKn _) -> Loc.ghost
+| CTacAtm (loc, _) -> Option.default dummy_loc loc
+| CTacRef (RelId (loc, _)) -> Option.default dummy_loc loc
+| CTacRef (AbsKn _) -> dummy_loc
 | CTacFun (loc, _, _) -> loc
 | CTacApp (loc, _, _) -> loc
 | CTacLet (loc, _, _, _) -> loc
-| CTacTup (loc, _) -> loc
-| CTacArr (loc, _) -> loc
-| CTacLst (loc, _) -> loc
+| CTacTup (loc, _) -> Option.default dummy_loc loc
+| CTacArr (loc, _) -> Option.default dummy_loc loc
+| CTacLst (loc, _) -> Option.default dummy_loc loc
 | CTacCnv (loc, _, _) -> loc
 | CTacSeq (loc, _, _) -> loc
 | CTacCse (loc, _, _) -> loc
@@ -206,7 +208,7 @@ let loc_of_tacexpr = function
 let loc_of_patexpr = function
 | CPatAny loc -> loc
 | CPatRef (loc, _, _) -> loc
-| CPatTup (loc, _) -> loc
+| CPatTup (loc, _) -> Option.default dummy_loc loc
 
 let error_nargs_mismatch loc nargs nfound =
   user_err ~loc (str "Constructor expects " ++ int nargs ++
@@ -226,7 +228,7 @@ let rec subst_type subst (t : 'a glb_typexpr) = match t with
   GTypRef (qid, List.map (fun t -> subst_type subst t) args)
 
 let rec intern_type env (t : raw_typexpr) : UF.elt glb_typexpr = match t with
-| CTypVar (loc, Name id) -> GTypVar (get_alias (loc, id) env)
+| CTypVar (loc, Name id) -> GTypVar (get_alias (Loc.tag ?loc id) env)
 | CTypVar (_, Anonymous) -> GTypVar (fresh_id env)
 | CTypRef (loc, rel, args) ->
   let (kn, nparams) = match rel with
@@ -238,7 +240,7 @@ let rec intern_type env (t : raw_typexpr) : UF.elt glb_typexpr = match t with
       let kn =
         try Tac2env.locate_type qid
         with Not_found ->
-          user_err ~loc (str "Unbound type constructor " ++ pr_qualid qid)
+          user_err ?loc (str "Unbound type constructor " ++ pr_qualid qid)
       in
       let (nparams, _) = Tac2env.interp_type kn in
       (kn, nparams)
@@ -251,9 +253,9 @@ let rec intern_type env (t : raw_typexpr) : UF.elt glb_typexpr = match t with
     if not (Int.equal nparams nargs) then
       let loc, qid = match rel with
       | RelId lid -> lid
-      | AbsKn kn -> loc, shortest_qualid_of_type kn
+      | AbsKn kn -> Some loc, shortest_qualid_of_type kn
       in
-      user_err ~loc (strbrk "The type constructor " ++ pr_qualid qid ++
+      user_err ?loc (strbrk "The type constructor " ++ pr_qualid qid ++
         strbrk " expects " ++ int nparams ++ strbrk " argument(s), but is here \
         applied to " ++ int nargs ++ strbrk "argument(s)")
   in
@@ -349,11 +351,11 @@ let rec unify env t1 t2 = match kind env t1, kind env t2 with
   else raise (CannotUnify (t1, t2))
 | _ -> raise (CannotUnify (t1, t2))
 
-let unify loc env t1 t2 =
+let unify ?loc env t1 t2 =
   try unify env t1 t2
   with CannotUnify (u1, u2) ->
     let name = env_name env in
-    user_err ~loc (str "This expression has type " ++ pr_glbtype name t1 ++
+    user_err ?loc (str "This expression has type " ++ pr_glbtype name t1 ++
       str " but an expression what expected of type " ++ pr_glbtype name t2)
 
 (** Term typing *)
@@ -481,7 +483,7 @@ let get_variable0 mem var = match var with
     let kn =
       try Tac2env.locate_ltac qid
       with Not_found ->
-        CErrors.user_err ~loc (str "Unbound value " ++ pr_qualid qid)
+        CErrors.user_err ?loc (str "Unbound value " ++ pr_qualid qid)
     in
     ArgArg kn
 | AbsKn kn -> ArgArg kn
@@ -498,12 +500,12 @@ let get_constructor env var = match var with
     let kn = Tac2env.interp_constructor knc in
     ArgArg (kn, knc)
   | Some (TacConstant _) ->
-    CErrors.user_err ~loc (str "The term " ++ pr_qualid qid ++
+    CErrors.user_err ?loc (str "The term " ++ pr_qualid qid ++
       str " is not the constructor of an inductive type.")
   | None ->
     let (dp, id) = repr_qualid qid in
     if DirPath.is_empty dp then ArgVar (loc, id)
-    else CErrors.user_err ~loc (str "Unbound constructor " ++ pr_qualid qid)
+    else CErrors.user_err ?loc (str "Unbound constructor " ++ pr_qualid qid)
   end
 | AbsKn knc ->
   let kn = Tac2env.interp_constructor knc in
@@ -512,7 +514,7 @@ let get_constructor env var = match var with
 let get_projection var = match var with
 | RelId (loc, qid) ->
   let kn = try Tac2env.locate_projection qid with Not_found ->
-    user_err ~loc (pr_qualid qid ++ str " is not a projection")
+    user_err ?loc (pr_qualid qid ++ str " is not a projection")
   in
   Tac2env.interp_projection kn
 | AbsKn kn ->
@@ -522,12 +524,12 @@ let intern_atm env = function
 | AtmInt n -> (GTacAtm (AtmInt n), GTypRef (t_int, []))
 | AtmStr s -> (GTacAtm (AtmStr s), GTypRef (t_string, []))
 
-let invalid_pattern ~loc kn t =
+let invalid_pattern ?loc kn t =
   let pt = match t with
   | GCaseAlg kn' -> pr_typref kn
   | GCaseTuple n -> str "tuple"
   in
-  user_err ~loc (str "Invalid pattern, expected a pattern for type " ++
+  user_err ?loc (str "Invalid pattern, expected a pattern for type " ++
     pr_typref kn ++ str ", found a pattern of type " ++ pt) (** FIXME *)
 
 (** Pattern view *)
@@ -547,7 +549,7 @@ let rec intern_patexpr env = function
 | CPatRef (_, qid, pl) ->
   begin match get_constructor env qid with
   | ArgVar (loc, id) ->
-    user_err ~loc (str "Unbound constructor " ++ Nameops.pr_id id)
+    user_err ?loc (str "Unbound constructor " ++ Nameops.pr_id id)
   | ArgArg (_, kn) -> GPatRef (kn, List.map (fun p -> intern_patexpr env p) pl)
   end
 | CPatTup (_, pl) ->
@@ -626,14 +628,14 @@ let rec intern_rec env = function
   in
   let ret = GTypVar (fresh_id env) in
   let (args, t) = List.fold_right fold args ([], ret) in
-  let () = unify loc env ft t in
+  let () = unify ~loc env ft t in
   (GTacApp (f, args), ret)
 | CTacLet (loc, false, el, e) ->
   let fold accu ((loc, na), _, _) = match na with
   | Anonymous -> accu
   | Name id ->
     if Id.Set.mem id accu then
-      user_err ~loc (str "Variable " ++ Id.print id ++ str " is bound several \
+      user_err ?loc (str "Variable " ++ Id.print id ++ str " is bound several \
         times in this matching")
     else Id.Set.add id accu
   in
@@ -644,7 +646,7 @@ let rec intern_rec env = function
     | None -> ()
     | Some tc ->
       let tc = intern_type env tc in
-      unify loc env t tc
+      unify ?loc env t tc
     in
     let t = if is_value e then abstract_var env t else monomorphic t in
     ((na, e) :: el), ((na, t) :: p)
@@ -683,7 +685,7 @@ let rec intern_rec env = function
 | CTacCnv (loc, e, tc) ->
   let (e, t) = intern_rec env e in
   let tc = intern_type env tc in
-  let () = unify loc env t tc in
+  let () = unify ~loc env t tc in
   (e, tc)
 | CTacSeq (loc, e1, e2) ->
   let (e1, t1) = intern_rec env e1 in
@@ -701,7 +703,7 @@ let rec intern_rec env = function
   let subst = Array.init pinfo.pdata_prms (fun _ -> fresh_id env) in
   let params = Array.map_to_list (fun i -> GTypVar i) subst in
   let exp = GTypRef (pinfo.pdata_type, params) in
-  let () = unify loc env t exp in
+  let () = unify ~loc env t exp in
   let substf i = GTypVar subst.(i) in
   let ret = subst_type substf pinfo.pdata_ptyp in
   (GTacPrj (pinfo.pdata_type, e, pinfo.pdata_indx), ret)
@@ -711,9 +713,9 @@ let rec intern_rec env = function
     if not pinfo.pdata_mutb then
       let loc = match proj with
       | RelId (loc, _) -> loc
-      | AbsKn _ -> Loc.ghost
+      | AbsKn _ -> None
       in
-      user_err ~loc (str "Field is not mutable")
+      user_err ?loc (str "Field is not mutable")
   in
   let subst = Array.init pinfo.pdata_prms (fun _ -> fresh_id env) in
   let params = Array.map_to_list (fun i -> GTypVar i) subst in
@@ -738,7 +740,7 @@ let rec intern_rec env = function
 and intern_rec_with_constraint env e exp =
   let loc = loc_of_tacexpr e in
   let (e, t) = intern_rec env e in
-  let () = unify loc env t exp in
+  let () = unify ~loc env t exp in
   e
 
 and intern_let_rec env loc el e =
@@ -746,7 +748,7 @@ and intern_let_rec env loc el e =
   | Anonymous -> accu
   | Name id ->
     if Id.Set.mem id accu then
-      user_err ~loc (str "Variable " ++ Id.print id ++ str " is bound several \
+      user_err ?loc (str "Variable " ++ Id.print id ++ str " is bound several \
         times in this matching")
     else Id.Set.add id accu
   in
@@ -765,12 +767,12 @@ and intern_let_rec env loc el e =
         user_err ~loc:loc_e (str "This kind of expression is not allowed as \
           right-hand side of a recursive binding")
     in
-    let () = unify loc env t (GTypVar id) in
+    let () = unify ?loc env t (GTypVar id) in
     let () = match tc with
     | None -> ()
     | Some tc ->
       let tc = intern_type env tc in
-      unify loc env t tc
+      unify ?loc env t tc
     in
     ((na, e) :: el, t :: tl)
   in
@@ -802,7 +804,7 @@ and intern_case env loc e pl =
     begin match pl with
     | [] -> assert false
     | [CPatTup (_, []), b] ->
-      let () = unify (loc_of_tacexpr e) env t (GTypRef (t_unit, [])) in
+      let () = unify ~loc:(loc_of_tacexpr e) env t (GTypRef (t_unit, [])) in
       let (b, tb) = intern_rec env b in
       (GTacCse (e', GCaseAlg t_unit, [|b|], [||]), tb)
     | [CPatTup (_, pl), b] ->
@@ -817,14 +819,14 @@ and intern_case env loc e pl =
       in
       let ids = Array.map_of_list map pl in
       let tc = GTypTuple (List.map (fun _ -> GTypVar (fresh_id env)) pl) in
-      let () = unify (loc_of_tacexpr e) env t tc in
+      let () = unify ~loc:(loc_of_tacexpr e) env t tc in
       let (b, tb) = intern_rec env b in
       (GTacCse (e', GCaseTuple len, [||], [|ids, b|]), tb)
     | (p, _) :: _ -> todo ~loc:(loc_of_patexpr p) ()
     end
   | PKind_variant kn ->
     let subst, tc = fresh_reftype env kn in
-    let () = unify (loc_of_tacexpr e) env t tc in
+    let () = unify ~loc:(loc_of_tacexpr e) env t tc in
     let (params, def) = Tac2env.interp_type kn in
     let cstrs = match def with
     | GTydAlg c -> c
@@ -911,9 +913,9 @@ and intern_case env loc e pl =
         in
         brT
       | CPatTup (loc, tup) ->
-        invalid_pattern ~loc kn (GCaseTuple (List.length tup))
+        invalid_pattern ?loc kn (GCaseTuple (List.length tup))
       in
-      let () = unify (loc_of_tacexpr br) env ret tbr in
+      let () = unify ~loc:(loc_of_tacexpr br) env ret tbr in
       intern_branch rem
     in
     let () = intern_branch pl in
@@ -927,7 +929,7 @@ and intern_case env loc e pl =
     (ce, ret)
   | PKind_open kn ->
     let subst, tc = fresh_reftype env kn in
-    let () = unify (loc_of_tacexpr e) env t tc in
+    let () = unify ~loc:(loc_of_tacexpr e) env t tc in
     let ret = GTypVar (fresh_id env) in
     let rec intern_branch map = function
     | [] ->
@@ -1002,7 +1004,7 @@ and intern_record env loc fs =
   let map (proj, e) =
     let loc = match proj with
     | RelId (loc, _) -> loc
-    | AbsKn _ -> Loc.ghost
+    | AbsKn _ -> None
     in
     let proj = get_projection proj in
     (loc, proj, e)
@@ -1029,10 +1031,10 @@ and intern_record env loc fs =
         args.(index) <- Some e
       | Some _ ->
         let (name, _, _) = List.nth typdef pinfo.pdata_indx in
-        user_err ~loc (str "Field " ++ Id.print name ++ str " is defined \
+        user_err ?loc (str "Field " ++ Id.print name ++ str " is defined \
           several times")
     else
-      user_err ~loc (str "Field " ++ (*KerName.print knp ++*) str " does not \
+      user_err ?loc (str "Field " ++ (*KerName.print knp ++*) str " does not \
         pertain to record definition " ++ pr_typref pinfo.pdata_type)
   in
   let () = List.iter iter fs in
@@ -1116,7 +1118,7 @@ let add_name accu = function
 let get_projection0 var = match var with
 | RelId (loc, qid) ->
   let kn = try Tac2env.locate_projection qid with Not_found ->
-    user_err ~loc (pr_qualid qid ++ str " is not a projection")
+    user_err ?loc (pr_qualid qid ++ str " is not a projection")
   in
   kn
 | AbsKn kn -> kn
diff --git a/tac2intern.mli b/src/tac2intern.mli
index 3d400a5cdd..3d400a5cdd 100644
--- a/tac2intern.mli
+++ b/src/tac2intern.mli
diff --git a/tac2interp.ml b/src/tac2interp.ml
index 664b7de3d6..664b7de3d6 100644
--- a/tac2interp.ml
+++ b/src/tac2interp.ml
diff --git a/tac2interp.mli b/src/tac2interp.mli
index bf6b2d4dde..bf6b2d4dde 100644
--- a/tac2interp.mli
+++ b/src/tac2interp.mli
diff --git a/tac2print.ml b/src/tac2print.ml
index e6f0582e3d..e6f0582e3d 100644
--- a/tac2print.ml
+++ b/src/tac2print.ml
diff --git a/tac2print.mli b/src/tac2print.mli
index ddd599641d..ddd599641d 100644
--- a/tac2print.mli
+++ b/src/tac2print.mli
diff --git a/Array.v b/theories/Array.v
index be4ab025ae..11b64e3515 100644
--- a/Array.v
+++ b/theories/Array.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Coq.ltac2.Init.
+Require Import Ltac2.Init.
 
 Ltac2 @external make : int -> 'a -> 'a array := "ltac2" "array_make".
 Ltac2 @external length : 'a array -> int := "ltac2" "array_length".
diff --git a/Constr.v b/theories/Constr.v
index 9e5833a778..c340e3aa87 100644
--- a/Constr.v
+++ b/theories/Constr.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Coq.ltac2.Init.
+Require Import Ltac2.Init.
 
 Ltac2 @ external type : constr -> constr := "ltac2" "constr_type".
 (** Return the type of a term *)
diff --git a/Control.v b/theories/Control.v
index 6b3b360abb..3bc572547c 100644
--- a/Control.v
+++ b/theories/Control.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Coq.ltac2.Init.
+Require Import Ltac2.Init.
 
 (** Panic *)
 
diff --git a/Init.v b/theories/Init.v
index 1d2d40f5c0..1d2d40f5c0 100644
--- a/Init.v
+++ b/theories/Init.v
diff --git a/Int.v b/theories/Int.v
index ab43eb27b0..0a90d757b6 100644
--- a/Int.v
+++ b/theories/Int.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Coq.ltac2.Init.
+Require Import Ltac2.Init.
 
 Ltac2 Type exn ::= [ Division_by_zero ].
 
diff --git a/Ltac2.v b/theories/Ltac2.v
index 625d4ac513..221f7be424 100644
--- a/Ltac2.v
+++ b/theories/Ltac2.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Export Coq.ltac2.Init.
+Require Export Ltac2.Init.
 
-Require Coq.ltac2.Int.
-Require Coq.ltac2.String.
-Require Coq.ltac2.Array.
-Require Coq.ltac2.Message.
-Require Coq.ltac2.Constr.
-Require Coq.ltac2.Control.
+Require Ltac2.Int.
+Require Ltac2.String.
+Require Ltac2.Array.
+Require Ltac2.Message.
+Require Ltac2.Constr.
+Require Ltac2.Control.
diff --git a/Message.v b/theories/Message.v
index 36233f4544..b2159612cb 100644
--- a/Message.v
+++ b/theories/Message.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Coq.ltac2.Init.
+Require Import Ltac2.Init.
 
 Ltac2 @ external print : message -> unit := "ltac2" "print".
 
diff --git a/String.v b/theories/String.v
index 3a4a178878..99e1dab76b 100644
--- a/String.v
+++ b/theories/String.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Coq.ltac2.Init.
+Require Import Ltac2.Init.
 
 Ltac2 @external make : int -> char -> string := "ltac2" "string_make".
 Ltac2 @external length : string -> int := "ltac2" "string_length".