diff options
| -rw-r--r-- | .gitignore | 14 | ||||
| -rw-r--r-- | LICENSE | 458 | ||||
| -rw-r--r-- | Makefile | 12 | ||||
| -rw-r--r-- | README.md | 0 | ||||
| -rw-r--r-- | _CoqProject | 28 | ||||
| -rw-r--r-- | src/g_ltac2.ml4 (renamed from g_ltac2.ml4) | 40 | ||||
| -rw-r--r-- | src/ltac2_plugin.mlpack (renamed from ltac2_plugin.mlpack) | 0 | ||||
| -rw-r--r-- | src/tac2core.ml (renamed from tac2core.ml) | 30 | ||||
| -rw-r--r-- | src/tac2core.mli (renamed from tac2core.mli) | 0 | ||||
| -rw-r--r-- | src/tac2entries.ml (renamed from tac2entries.ml) | 45 | ||||
| -rw-r--r-- | src/tac2entries.mli (renamed from tac2entries.mli) | 0 | ||||
| -rw-r--r-- | src/tac2env.ml (renamed from tac2env.ml) | 0 | ||||
| -rw-r--r-- | src/tac2env.mli (renamed from tac2env.mli) | 0 | ||||
| -rw-r--r-- | src/tac2expr.mli (renamed from tac2expr.mli) | 0 | ||||
| -rw-r--r-- | src/tac2intern.ml (renamed from tac2intern.ml) | 86 | ||||
| -rw-r--r-- | src/tac2intern.mli (renamed from tac2intern.mli) | 0 | ||||
| -rw-r--r-- | src/tac2interp.ml (renamed from tac2interp.ml) | 0 | ||||
| -rw-r--r-- | src/tac2interp.mli (renamed from tac2interp.mli) | 0 | ||||
| -rw-r--r-- | src/tac2print.ml (renamed from tac2print.ml) | 0 | ||||
| -rw-r--r-- | src/tac2print.mli (renamed from tac2print.mli) | 0 | ||||
| -rw-r--r-- | theories/Array.v (renamed from Array.v) | 2 | ||||
| -rw-r--r-- | theories/Constr.v (renamed from Constr.v) | 2 | ||||
| -rw-r--r-- | theories/Control.v (renamed from Control.v) | 2 | ||||
| -rw-r--r-- | theories/Init.v (renamed from Init.v) | 0 | ||||
| -rw-r--r-- | theories/Int.v (renamed from Int.v) | 2 | ||||
| -rw-r--r-- | theories/Ltac2.v (renamed from Ltac2.v) | 14 | ||||
| -rw-r--r-- | theories/Message.v (renamed from Message.v) | 2 | ||||
| -rw-r--r-- | theories/String.v (renamed from String.v) | 2 |
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". |