diff -Nru coq-doc-8.4pl2/CHANGES coq-doc-8.4pl4/CHANGES --- coq-doc-8.4pl2/CHANGES 2013-04-02 08:05:37.000000000 +0000 +++ coq-doc-8.4pl4/CHANGES 2014-04-24 15:13:03.000000000 +0000 @@ -1,3 +1,74 @@ +Changes from V8.4pl3 to V8.4pl4 +=============================== + +WARNING: +The current logic of Coq is now known to be inconsistent with + Axiom prop_extensionality : forall A B:Prop, (A <-> B) -> A = B. +For more details, see: + https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq/coq.git;a=blob_plain;f=test-suite/failure/subterm2.v;hb=HEAD +or + https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq/coq.git;a=blob_plain;f=test-suite/failure/subterm3.v;hb=HEAD + +Kernel + +- Bug #3211: unsound check of elimination sort. +- Fix guard condition for nested cofixpoints. +- Bug #3243: Univ constraints of module subtyping were not propagated. + +Tactics + +- A new option "Set Stable Omega" ensures that repeated identical calls + to omega will produce identical proof terms. This option is off by default + for maximal compatibility, but should be pretty safe to activate. +- The interpretation of the open_constr tactic argument was erroneously + firing type classes resolution in some corner cases. This has been + fixed. The tactic argument type open_constr_wTC is provided for retro + compatibility purposes. +- Fixing bug #3228 (fixing precedence of ltac variables over variables in + env) introduces rare and justified tactic failure. + +Bug fixes + +- Solved bugs: + #3260, #2697, #3037, #3262, #2900, #3131, #3238, #3204, #1758, #1039, + #3144 +- micromega: solved an ambiguous symbol resolution. +- Coq always uses / as separator between directories on all platforms. +- remove trailing '\r' from file names returned by coqtop. +- bug correction in proving inversion principles for Function. +- ocamlbuild: minor fixes related to camlp4 and cross-compilation. + +Changes from V8.4pl2 to V8.4pl3 +=============================== + +Ide_slave XML interface + +- 20120712, 20130419 : Invalidated protocol versions +- From 20130419 extra datastructure : union + (Inl "" = , + Inr _ = ...) +- 20130419~1 : new toplevel entry : message, not send by coptop v8.4 and not + handle by coqide v8.4. A message has a level and a content (of string). + Message levels are Debug of string, Info, Notice, Warning and Error. +- 20130425 : + * new toplevel entry : feedback, once again not send by coqtop v8.4 and not + handle by coqide v8.4. A feedback gives the id of the sentence it provides info + about and a content. Feedback contents are Processed, AddedAxiom and + GlobRef of Util.loc * string * string * string * string + * must provide an attribute id of type int. It is OK in + coqtop v8.4 to alwais send + +Bug fixes + +- Solved bugs: + #2230 #2837 #2846 #2987 #3003 #3001 #3013 #3023 #3025 #3036 #3118 #3169 + #(3150, 3151, 3152, 3153) +- Fixing a significant efficiency leak in the code of the field tactic. +- Fix caching of local hint database in typeclasses eauto which could + miss some hypotheses. +- Fix automatic solving of obligation in program, which was not trying + to solve obligations that had no undefined dependencies left. + Changes from V8.4pl1 to V8.4pl2 =============================== diff -Nru coq-doc-8.4pl2/checker/checker.ml coq-doc-8.4pl4/checker/checker.ml --- coq-doc-8.4pl2/checker/checker.ml 2013-02-13 17:19:16.000000000 +0000 +++ coq-doc-8.4pl4/checker/checker.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* raise (LocalArity None)); srec (push_rel (na1,None,a1) env) t ar' - | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *) - let ksort = match (whd_betadeltaiota env a2) with - | Sort s -> family_of_sort s + | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) + let env' = push_rel (na1,None,a1) env in + let ksort = match (whd_betadeltaiota env' a2) with + | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in let dep_ind = build_dependent_inductive ind specif params in (try conv env a1 dep_ind @@ -289,6 +290,8 @@ | Sort s', [] -> check_allowed_sort (family_of_sort s') specif; false + | _, (_,Some _,_ as d)::ar' -> + srec (push_rel d env) (lift 1 pt') ar' | _ -> raise (LocalArity None) in @@ -895,12 +898,12 @@ raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) | CoFix (j,(_,varit,vdefs as recdef)) -> - if (List.for_all (noccur_with_meta n nbfix) args) + if List.for_all (noccur_with_meta n nbfix) args then - let nbfix = Array.length vdefs in - if (array_for_all (noccur_with_meta n nbfix) varit) then + if array_for_all (noccur_with_meta n nbfix) varit then + let nbfix = Array.length vdefs in let env' = push_rec_types recdef env in - (Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs; + (Array.iter (check_rec_call env' alreadygrd (n+nbfix) vlra) vdefs; List.iter (check_rec_call env alreadygrd n vlra) args) else raise (CoFixGuardError (env,RecCallInTypeOfDef c)) diff -Nru coq-doc-8.4pl2/checker/inductive.mli coq-doc-8.4pl4/checker/inductive.mli --- coq-doc-8.4pl2/checker/inductive.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/checker/inductive.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* /dev/null); then + # Beware of the final \r in Win32 + lablgtkdirtmp="$(ocamlfind query lablgtk2 2> /dev/null | tr -d '\r')" + if [ "$lablgtkdirtmp" != "" ]; then if [ -f "$lablgtkdirtmp/glib.cmi" -a -f "$lablgtkdirtmp/glib.mli" ]; then lablgtkdirfoundmsg="LabelGtk2 found by ocamlfind" lablgtkdir=$lablgtkdirtmp @@ -632,7 +642,7 @@ echo "Headers missings in Lablgtk2 found by ocamlfind (glib.cmi/glib.mli not found)." fi fi - if [ "$lablgtkdir" = "" -a -f "${CAMLLIB}/lablgtk2/glib.mli" -a -f "${CAMLLIB}/glib.mli" ]; then + if [ "$lablgtkdir" = "" -a -f "${CAMLLIB}/lablgtk2/glib.cmi" -a -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then lablgtkdirfoundmsg="LablGtk2 found in ocaml lib directory" lablgtkdir=${CAMLLIB}/lablgtk2 LABLGTKLIB=+lablgtk2 # Pour le message utilisateur @@ -887,7 +897,7 @@ */true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$COQTOP'/kernel/byterun";; *) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'" - BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun";; + BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun:$CAML_LD_LIBRARY_PATH";; esac case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";; diff -Nru coq-doc-8.4pl2/debian/changelog coq-doc-8.4pl4/debian/changelog --- coq-doc-8.4pl2/debian/changelog 2013-12-12 08:06:18.000000000 +0000 +++ coq-doc-8.4pl4/debian/changelog 2014-08-17 12:36:07.000000000 +0000 @@ -1,3 +1,12 @@ +coq-doc (8.4pl4-1) unstable; urgency=medium + + * New upstream release + * Update debian/watch + * Put debian/copyright in format 1.0 + * Bump Standards-Version to 3.9.5 + + -- Stéphane Glondu Sun, 17 Aug 2014 14:36:07 +0200 + coq-doc (8.4pl2-1) unstable; urgency=medium * New upstream release diff -Nru coq-doc-8.4pl2/debian/control coq-doc-8.4pl4/debian/control --- coq-doc-8.4pl2/debian/control 2013-12-12 07:17:30.000000000 +0000 +++ coq-doc-8.4pl4/debian/control 2014-08-17 12:35:10.000000000 +0000 @@ -5,7 +5,7 @@ Uploaders: Samuel Mimram , Stéphane Glondu -Standards-Version: 3.9.2 +Standards-Version: 3.9.5 Build-Depends: debhelper (>= 9) Build-Depends-Indep: texlive, diff -Nru coq-doc-8.4pl2/debian/copyright coq-doc-8.4pl4/debian/copyright --- coq-doc-8.4pl2/debian/copyright 2013-12-12 07:08:37.000000000 +0000 +++ coq-doc-8.4pl4/debian/copyright 2014-08-17 12:34:16.000000000 +0000 @@ -1,232 +1,221 @@ +Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ Packaged-By: Fernando Sanchez Packaged-Date: Sun, 28 Nov 1999 19:42:06 +0100 Upstream-Author: The Coq Development Team -Original-Source-Location: http://coq.inria.fr/ - - - Note: The Coq proof assistant itself is DFSG-free and packaged in - Debian (main). However, its documentation is under OPL, a license - which is not considered DFSG-free. See: - - http://lists.debian.org/debian-legal/2004/03/msg00226.html - +Source: http://coq.inria.fr/ +Comment: + The Coq proof assistant itself is DFSG-free and packaged in Debian + (main). However, its documentation is under OPL, a license which is + not considered DFSG-free. See: + http://lists.debian.org/debian-legal/2004/03/msg00226.html Files: * -Copyright: © 1999-2004 The Coq development team, - INRIA-CNRS, University Paris Sud +Copyright: 1999-2004, The Coq development team, INRIA-CNRS, University Paris Sud License: LGPL-2.1 - - The Coq proof assistant is distributed under the terms of the GNU - Lesser General Public License, version 2.1. On Debian systems, the - full text can be found in /usr/share/common-licenses/LGPL-2.1. - - The Coq proof assistant V7 and V8 includes software developed by the - Coq development team inside the TypiCal (formerly LogiCal) project, - at INRIA, CNRS and University Paris Sud. - - Copyright 1999-2004 The Coq development team, INRIA-CNRS, University - Paris Sud, All rights reserved. - - This product includes also software developed by many external - contributors, see /usr/share/coq-doc/CREDITS.gz and the credits - section in the introduction of the Reference Manual. +Comment: + This product includes also software developed by many external + contributors, see /usr/share/coq-doc/CREDITS.gz and the credits + section in the introduction of the Reference Manual. Files: doc/refman/* -Copyright: © 1999-2006 INRIA -License: other - - The Coq Reference Manual is a collective work from the Coq - Development Team whose members are listed in the file CREDITS of the - Coq source package. All related documents (the LaTeX and BibTeX - sources, the embedded png files, and the PostScript, PDF and html - outputs) are copyright (c) INRIA 1999-2006. The material connected - to the Reference Manual may be distributed only subject to the terms - and conditions set forth in the Open Publication License, v1.0 or - later (the latest version is presently available at - http://www.opencontent.org/openpub/). Options A and B are *not* - elected. +Copyright: 1999-2006, INRIA +License: OPL-1.0 +Comment: + The Coq Reference Manual is a collective work from the Coq + Development Team whose members are listed in the file CREDITS of the + Coq source package. All related documents (the LaTeX and BibTeX + sources, the embedded png files, and the PostScript, PDF and html + outputs) are copyright (c) INRIA 1999-2006. The material connected + to the Reference Manual may be distributed only subject to the terms + and conditions set forth in the Open Publication License, v1.0 or + later (the latest version is presently available at + http://www.opencontent.org/openpub/). Options A and B are *not* + elected. Files: doc/tutorial/* -Copyright: © 1999-2006 INRIA -License: other - - The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine - Paulin-Mohring. All documents (the LaTeX source and the PostScript, - PDF and html outputs) are copyright (c) INRIA 1999-2006. The - material connected to the Coq Tutorial may be distributed only - subject to the terms and conditions set forth in the Open - Publication License, v1.0 or later (the latest version is presently - available at http://www.opencontent.org/openpub/). Options A and B - are *not* elected. +Copyright: 1999-2006, INRIA +License: OPL-1.0 +Comment: + The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine + Paulin-Mohring. All documents (the LaTeX source and the PostScript, + PDF and html outputs) are copyright (c) INRIA 1999-2006. The + material connected to the Coq Tutorial may be distributed only + subject to the terms and conditions set forth in the Open + Publication License, v1.0 or later (the latest version is presently + available at http://www.opencontent.org/openpub/). Options A and B + are *not* elected. Files: doc/stdlib/* -Copyright: © 1999-2006 INRIA -License: other - - The Coq Standard Library is a collective work from the Coq - Development Team whose members are listed in the file CREDITS of the - Coq source package. All related documents (the Coq vernacular source - files and the PostScript, PDF and html outputs) are copyright (c) - INRIA 1999-2006. The material connected to the Standard Library is - distributed under the terms of the Lesser General Public License - version 2.1 or later. +Copyright: 1999-2006, INRIA +License: LGPL-2.1 +Comment: + The Coq Standard Library is a collective work from the Coq + Development Team whose members are listed in the file CREDITS of the + Coq source package. All related documents (the Coq vernacular source + files and the PostScript, PDF and html outputs) are copyright (c) + INRIA 1999-2006. The material connected to the Standard Library is + distributed under the terms of the Lesser General Public License + version 2.1 or later. Files: doc/faq/* -Copyright: © 2004-2006 INRIA -License: other - - The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo - Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All - documents (the LaTeX source and the PostScript, PDF and html - outputs) are copyright (c) INRIA 2004-2006. The material connected - to the FAQ (Coq for the Clueless) may be distributed only subject to - the terms and conditions set forth in the Open Publication License, - v1.0 or later (the latest version is presently available at - http://www.opencontent.org/openpub/). Options A and B are *not* - elected. +Copyright: 2004-2006, INRIA +License: OPL-1.0 +Comment: + The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo + Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All + documents (the LaTeX source and the PostScript, PDF and html + outputs) are copyright (c) INRIA 2004-2006. The material connected + to the FAQ (Coq for the Clueless) may be distributed only subject to + the terms and conditions set forth in the Open Publication License, + v1.0 or later (the latest version is presently available at + http://www.opencontent.org/openpub/). Options A and B are *not* + elected. Files: doc/RecTutorial/* -Copyright: © 1997-2006 INRIA -License: other - - The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre - Castéran and Eduardo Gimenez. All related documents (the LaTeX and - BibTeX sources and the PostScript, PDF and html outputs) are - copyright (c) INRIA 1997-2006. The material connected to the - Tutorial on [Co-]Inductive Types in Coq may be distributed only - subject to the terms and conditions set forth in the Open - Publication License, v1.0 or later (the latest version is presently - available at http://www.opencontent.org/openpub/). Options A and B - are *not* elected. +Copyright: 1997-2006, INRIA +License: OPL-1.0 +Comment: + The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre + Castéran and Eduardo Gimenez. All related documents (the LaTeX and + BibTeX sources and the PostScript, PDF and html outputs) are + copyright (c) INRIA 1997-2006. The material connected to the + Tutorial on [Co-]Inductive Types in Coq may be distributed only + subject to the terms and conditions set forth in the Open + Publication License, v1.0 or later (the latest version is presently + available at http://www.opencontent.org/openpub/). Options A and B + are *not* elected. Files: debian/* -Copyright: © 1999 Fernando Sanchez - © 2002 Judicaël Courant - © 2004-2010 Samuel Mimram - © 2010 Stéphane Glondu +Copyright: 1999, Fernando Sanchez + 2002, Judicaël Courant + 2004-2010, Samuel Mimram + 2010-2014, Stéphane Glondu License: LGPL-2.1 ----------------------------------------------------------------------- - - *Open Publication License* - v1.0, 8 June 1999 - - -*I. REQUIREMENTS ON BOTH UNMODIFIED AND MODIFIED VERSIONS* - -The Open Publication works may be reproduced and distributed in whole or -in part, in any medium physical or electronic, provided that the terms -of this license are adhered to, and that this license or an -incorporation of it by reference (with any options elected by the -author(s) and/or publisher) is displayed in the reproduction. - -Proper form for an incorporation by reference is as follows: - - Copyright (c) by . This material - may be distributed only subject to the terms and conditions set - forth in the Open Publication License, vX.Y or later (the latest - version is presently available at http://www.opencontent.org/openpub/). - -The reference must be immediately followed with any options elected by -the author(s) and/or publisher of the document (see section VI). - -Commercial redistribution of Open Publication-licensed material is -permitted. - -Any publication in standard (paper) book form shall require the citation -of the original publisher and author. The publisher and author's names -shall appear on all outer surfaces of the book. On all outer surfaces of -the book the original publisher's name shall be as large as the title of -the work and cited as possessive with respect to the title. - - -*II. COPYRIGHT* - -The copyright to each Open Publication is owned by its author(s) or -designee. - - -*III. SCOPE OF LICENSE* - -The following license terms apply to all Open Publication works, unless -otherwise explicitly stated in the document. - -Mere aggregation of Open Publication works or a portion of an Open -Publication work with other works or programs on the same media shall -not cause this license to apply to those other works. The aggregate work -shall contain a notice specifying the inclusion of the Open Publication -material and appropriate copyright notice. - -SEVERABILITY. If any part of this license is found to be unenforceable -in any jurisdiction, the remaining portions of the license remain in force. - -NO WARRANTY. Open Publication works are licensed and provided "as is" -without warranty of any kind, express or implied, including, but not -limited to, the implied warranties of merchantability and fitness for a -particular purpose or a warranty of non-infringement. - - -*IV. REQUIREMENTS ON MODIFIED WORKS* - -All modified versions of documents covered by this license, including -translations, anthologies, compilations and partial documents, must meet -the following requirements: - - 1. The modified version must be labeled as such. - 2. The person making the modifications must be identified and the - modifications dated. - 3. Acknowledgement of the original author and publisher if applicable - must be retained according to normal academic citation practices. - 4. The location of the original unmodified document must be identified. - 5. The original author's (or authors') name(s) may not be used to - assert or imply endorsement of the resulting document without the - original author's (or authors') permission. - - -*V. GOOD-PRACTICE RECOMMENDATIONS * - -In addition to the requirements of this license, it is requested from -and strongly recommended of redistributors that: - - 1. If you are distributing Open Publication works on hardcopy or - CD-ROM, you provide email notification to the authors of your - intent to redistribute at least thirty days before your manuscript - or media freeze, to give the authors time to provide updated - documents. This notification should describe modifications, if - any, made to the document. - 2. All substantive modifications (including deletions) be either - clearly marked up in the document or else described in an - attachment to the document. - 3. Finally, while it is not mandatory under this license, it is - considered good form to offer a free copy of any hardcopy and - CD-ROM expression of an Open Publication-licensed work to its - author(s). - - -*VI. LICENSE OPTIONS* - -The author(s) and/or publisher of an Open Publication-licensed document -may elect certain options by appending language to the reference to or -copy of the license. These options are considered part of the license -instance and must be included with the license (or its incorporation by -reference) in derived works. - -A. To prohibit distribution of substantively modified versions without -the explicit permission of the author(s). "Substantive modification" is -defined as a change to the semantic content of the document, and -excludes mere changes in format or typographical corrections. - -To accomplish this, add the phrase `Distribution of substantively -modified versions of this document is prohibited without the explicit -permission of the copyright holder.' to the license reference or copy. - -B. To prohibit any publication of this work or derivative works in whole -or in part in standard (paper) book form for commercial purposes is -prohibited unless prior permission is obtained from the copyright holder. - -To accomplish this, add the phrase 'Distribution of the work or -derivative of the work in any standard (paper) book form is prohibited -unless prior permission is obtained from the copyright holder.' to the -license reference or copy. - ----------------------------------------------------------------------- +License: LGPL-2.1 + This software is distributed under the terms of the GNU Lesser + General Public License, version 2.1. On Debian systems, the full text + can be found in /usr/share/common-licenses/LGPL-2.1. + +License: OPL-1.0 + . + *Open Publication License* + v1.0, 8 June 1999 + . + . + *I. REQUIREMENTS ON BOTH UNMODIFIED AND MODIFIED VERSIONS* + . + The Open Publication works may be reproduced and distributed in whole or + in part, in any medium physical or electronic, provided that the terms + of this license are adhered to, and that this license or an + incorporation of it by reference (with any options elected by the + author(s) and/or publisher) is displayed in the reproduction. + . + Proper form for an incorporation by reference is as follows: + . + Copyright (c) by . This material + may be distributed only subject to the terms and conditions set + forth in the Open Publication License, vX.Y or later (the latest + version is presently available at http://www.opencontent.org/openpub/). + . + The reference must be immediately followed with any options elected by + the author(s) and/or publisher of the document (see section VI). + . + Commercial redistribution of Open Publication-licensed material is + permitted. + . + Any publication in standard (paper) book form shall require the citation + of the original publisher and author. The publisher and author's names + shall appear on all outer surfaces of the book. On all outer surfaces of + the book the original publisher's name shall be as large as the title of + the work and cited as possessive with respect to the title. + . + . + *II. COPYRIGHT* + . + The copyright to each Open Publication is owned by its author(s) or + designee. + . + . + *III. SCOPE OF LICENSE* + . + The following license terms apply to all Open Publication works, unless + otherwise explicitly stated in the document. + . + Mere aggregation of Open Publication works or a portion of an Open + Publication work with other works or programs on the same media shall + not cause this license to apply to those other works. The aggregate work + shall contain a notice specifying the inclusion of the Open Publication + material and appropriate copyright notice. + . + SEVERABILITY. If any part of this license is found to be unenforceable + in any jurisdiction, the remaining portions of the license remain in force. + . + NO WARRANTY. Open Publication works are licensed and provided "as is" + without warranty of any kind, express or implied, including, but not + limited to, the implied warranties of merchantability and fitness for a + particular purpose or a warranty of non-infringement. + . + . + *IV. REQUIREMENTS ON MODIFIED WORKS* + . + All modified versions of documents covered by this license, including + translations, anthologies, compilations and partial documents, must meet + the following requirements: + . + 1. The modified version must be labeled as such. + 2. The person making the modifications must be identified and the + modifications dated. + 3. Acknowledgement of the original author and publisher if applicable + must be retained according to normal academic citation practices. + 4. The location of the original unmodified document must be identified. + 5. The original author's (or authors') name(s) may not be used to + assert or imply endorsement of the resulting document without the + original author's (or authors') permission. + . + . + *V. GOOD-PRACTICE RECOMMENDATIONS * + . + In addition to the requirements of this license, it is requested from + and strongly recommended of redistributors that: + . + 1. If you are distributing Open Publication works on hardcopy or + CD-ROM, you provide email notification to the authors of your + intent to redistribute at least thirty days before your manuscript + or media freeze, to give the authors time to provide updated + documents. This notification should describe modifications, if + any, made to the document. + 2. All substantive modifications (including deletions) be either + clearly marked up in the document or else described in an + attachment to the document. + 3. Finally, while it is not mandatory under this license, it is + considered good form to offer a free copy of any hardcopy and + CD-ROM expression of an Open Publication-licensed work to its + author(s). + . + . + *VI. LICENSE OPTIONS* + . + The author(s) and/or publisher of an Open Publication-licensed document + may elect certain options by appending language to the reference to or + copy of the license. These options are considered part of the license + instance and must be included with the license (or its incorporation by + reference) in derived works. + . + A. To prohibit distribution of substantively modified versions without + the explicit permission of the author(s). "Substantive modification" is + defined as a change to the semantic content of the document, and + excludes mere changes in format or typographical corrections. + . + To accomplish this, add the phrase `Distribution of substantively + modified versions of this document is prohibited without the explicit + permission of the copyright holder.' to the license reference or copy. + . + B. To prohibit any publication of this work or derivative works in whole + or in part in standard (paper) book form for commercial purposes is + prohibited unless prior permission is obtained from the copyright holder. + . + To accomplish this, add the phrase 'Distribution of the work or + derivative of the work in any standard (paper) book form is prohibited + unless prior permission is obtained from the copyright holder.' to the + license reference or copy. diff -Nru coq-doc-8.4pl2/debian/watch coq-doc-8.4pl4/debian/watch --- coq-doc-8.4pl2/debian/watch 2013-12-12 07:08:37.000000000 +0000 +++ coq-doc-8.4pl4/debian/watch 2014-08-17 12:22:30.000000000 +0000 @@ -1,3 +1,3 @@ version=3 -http://coq.inria.fr/download distrib/[^/]+/files/coq-(.*)\.tar\.gz +http://coq.inria.fr/download .*/coq-(.*)\.tar\.gz diff -Nru coq-doc-8.4pl2/dev/db_printers.ml coq-doc-8.4pl4/dev/db_printers.ml --- coq-doc-8.4pl2/dev/db_printers.ml 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/dev/db_printers.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* X -> X. +Definition TRUE : BOOL := fun X x1 x2 => x1. +Definition FALSE : BOOL := fun X x1 x2 => x2. +Definition EQBOOL (x1 x2:BOOL) := forall P:BOOL->Set, P x1 -> P x2. +Definition BOT := forall X:Set, X. + +Definition BOOL2bool : BOOL -> bool := fun b => b bool true false. + +Theorem DISCR : EQBOOL TRUE FALSE -> BOT. +intro X. +assert (H : BOOL2bool TRUE = BOOL2bool FALSE). +{ apply X. trivial. } +discriminate H. +Qed. +\end{coq_example*} + +If the impredicative sort of CC is interpreted as {\Prop}, CIC is +presumably conservative over CC. The general idea is that no +proof-relevant information can flow from {\Prop} to {\Set}, even +though singleton elimination can be used. Hence types in {\Set} should +be smashable to the unit type and {\Set} and {\Type} themselves be +mapped to {\Prop}. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Talkin' with the Rooster} @@ -1211,11 +1244,9 @@ These two commands perform type checking, but when {\Defined} is used the new definition is set as transparent, otherwise it is defined as opaque (see \ref{opaque}). -\Question{How can I know what a tactic does?} - -You can use the {\tt info} command. - +\Question{How can I know what an automation tactic does in my example?} +You can use its {\tt info} variant: info\_auto, info\_trivial, info\_eauto. \Question{Why {\auto} does not work? How can I fix it?} @@ -1228,7 +1259,7 @@ \Question{How can I speed up {\auto}?} -You can use \texttt{info }{\auto} to replace {\auto} by the tactics it generates. +You can use \texttt{info\_}{\auto} to replace {\auto} by the tactics it generates. You can split your hint bases into smaller ones. diff -Nru coq-doc-8.4pl2/doc/refman/Polynom.tex coq-doc-8.4pl4/doc/refman/Polynom.tex --- coq-doc-8.4pl2/doc/refman/Polynom.tex 2012-07-08 23:52:41.000000000 +0000 +++ coq-doc-8.4pl4/doc/refman/Polynom.tex 2014-04-24 15:13:03.000000000 +0000 @@ -222,7 +222,9 @@ closed expressions when operations are effective. It consists in introducing a type of \emph{coefficients} and an implementation of the ring operations, and a morphism from the coefficient type to the ring -carrier type. The morphism needs not be injective, nor surjective. As +carrier type. The morphism needs not be injective, nor surjective. + +As an example, one can consider the real numbers. The set of coefficients could be the rational numbers, upon which the ring operations can be implemented. The fact that there exists a morphism is defined by the @@ -250,7 +252,15 @@ {\tt +!}, {\tt *!}, {\tt -!} are the implementations of the ring operations, {\tt ==} is the equality of the coefficients, {\tt ?+!} is an implementation of this equality, and {\tt [x]} is a notation for -the image of {\tt x} by the ring morphism. +the image of {\tt x} by the ring morphism. Moreover, the term +{\tt [c0]} (resp. {\tt [c1]}), image by the morphism of the 0 +(resp. the 1) of the coefficient set, +should be \emph{convertible} to the term {\tt 0} (resp. the term +{\tt 1}) of the ring structure. This requirement is not enforced by +the command registering a new ring but the tactic is otherwise very +much incomplete. + + Since {\tt Z} is an initial ring (and {\tt N} is an initial semi-ring), it can always be considered as a set of diff -Nru coq-doc-8.4pl2/doc/refman/RefMan-ext.tex coq-doc-8.4pl4/doc/refman/RefMan-ext.tex --- coq-doc-8.4pl2/doc/refman/RefMan-ext.tex 2013-02-21 16:39:41.000000000 +0000 +++ coq-doc-8.4pl4/doc/refman/RefMan-ext.tex 2014-04-24 15:13:03.000000000 +0000 @@ -517,6 +517,7 @@ The default is to not print synthesizable types. \subsubsection{Printing matching on irrefutable pattern +\label{AddPrintingLet} \comindex{Add Printing Let {\ident}} \comindex{Remove Printing Let {\ident}} \comindex{Test Printing Let for {\ident}} diff -Nru coq-doc-8.4pl2/doc/refman/RefMan-ltac.tex coq-doc-8.4pl4/doc/refman/RefMan-ltac.tex --- coq-doc-8.4pl2/doc/refman/RefMan-ltac.tex 2012-07-08 23:52:41.000000000 +0000 +++ coq-doc-8.4pl4/doc/refman/RefMan-ltac.tex 2014-04-24 15:13:03.000000000 +0000 @@ -68,7 +68,7 @@ a term, use the syntax {\tt ({\qualid})}. \item As shown by the figure, tactical {\tt ||} binds more than the -prefix tacticals {\tt try}, {\tt repeat}, {\tt do}, {\tt info} and +prefix tacticals {\tt try}, {\tt repeat}, {\tt do} and {\tt abstract} which themselves bind more than the postfix tactical ``{\tt \dots\ ;[ \dots\ ]}'' which binds more than ``\dots\ {\tt ;} \dots''. @@ -96,7 +96,6 @@ \\ {\tacexprpref} & ::= & {\tt do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\ -& | & {\tt info} {\tacexprpref}\\ & | & {\tt progress} {\tacexprpref}\\ & | & {\tt repeat} {\tacexprpref}\\ & | & {\tt try} {\tacexprpref}\\ @@ -770,14 +769,6 @@ {\tt type of} {\term} \end{quote} -\subsubsection[Accessing tactic decomposition]{Accessing tactic decomposition\tacindex{info} -\index{Tacticals!info@{\tt info}}} - -Tactical ``{\tt info} {\tacexpr}'' is not really a tactical. For -elementary tactics, this is equivalent to \tacexpr. For complex tactic -like \texttt{auto}, it displays the operations performed by the -tactic. - \subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract} \index{Tacticals!abstract@{\tt abstract}}} diff -Nru coq-doc-8.4pl2/doc/refman/RefMan-oth.tex coq-doc-8.4pl4/doc/refman/RefMan-oth.tex --- coq-doc-8.4pl2/doc/refman/RefMan-oth.tex 2012-08-03 14:22:43.000000000 +0000 +++ coq-doc-8.4pl4/doc/refman/RefMan-oth.tex 2014-04-24 15:13:03.000000000 +0000 @@ -51,26 +51,24 @@ %% was introduced. \end{Variants} -\section{Options and Flags} -\subsection[\tt Set {\rm\sl option} {\rm\sl value}.]{\tt Set {\rm\sl option} {\rm\sl value}.\comindex{Set}} -This command sets {\rm\sl option} to {\rm\sl value}. The original value of -{\rm\sl option} is restored when the current module ends. +\section{Flags, Options and Tables} -\begin{Variants} -\item {\tt Set {\rm\sl flag}.}\\ +{\Coq} configurability is based on flags (e.g. {\tt Set Printing All} in +Section~\ref{SetPrintingAll}), options (e.g. {\tt Set Printing Width + {\integer}} in Section~\ref{SetPrintingWidth}), or tables (e.g. {\tt + Add Printing Record {\ident}}, in Section~\ref{AddPrintingLet}). The +names of flags, options and tables are made of non-empty sequences of +identifiers (conventionally with capital initial letter). The general +commands handling flags, options and tables are given below. + +\subsection[\tt Set {\rm\sl flag}.]{\tt Set {\rm\sl flag}.\comindex{Set}} This command switches {\rm\sl flag} on. The original state of {\rm\sl flag} is restored when the current module ends. -\item {\tt Local Set {\rm\sl option} {\rm\sl value}.\comindex{Local Set}} -This command sets {\rm\sl option} to {\rm\sl value}. The original value of -{\rm\sl option} is restored when the current \emph{section} ends. + +\begin{Variants} \item {\tt Local Set {\rm\sl flag}.}\\ This command switches {\rm\sl flag} on. The original state of {\rm\sl flag} is restored when the current \emph{section} ends. -\item {\tt Global Set {\rm\sl option} {\rm\sl value}.\comindex{Global Set}} -This command sets {\rm\sl option} to {\rm\sl value}. The original value of -{\rm\sl option} is \emph{not} restored at the end of the module. Additionally, -if set in a file, {\rm\sl option} is set to {\rm\sl value} when the file is -{\tt Require}-d. \item {\tt Global Set {\rm\sl flag}.}\\ This command switches {\rm\sl flag} on. The original state of {\rm\sl flag} is \emph{not} restored at the end of the module. Additionally, @@ -93,12 +91,52 @@ {\tt Require}-d. \end{Variants} +\subsection[\tt Test {\rm\sl flag}.]{\tt Test {\rm\sl flag}.\comindex{Test}} +This command prints whether {\rm\sl flag} is on or off. + +\subsection[\tt Set {\rm\sl option} {\rm\sl value}.]{\tt Set {\rm\sl option} {\rm\sl value}.\comindex{Set}} +This command sets {\rm\sl option} to {\rm\sl value}. The original value of +{\rm\sl option} is restored when the current module ends. + +\begin{Variants} +\item {\tt Local Set {\rm\sl option} {\rm\sl value}.\comindex{Local Set}} +This command sets {\rm\sl option} to {\rm\sl value}. The original value of +\item {\tt Global Set {\rm\sl option} {\rm\sl value}.\comindex{Global Set}} +This command sets {\rm\sl option} to {\rm\sl value}. The original value of +{\rm\sl option} is \emph{not} restored at the end of the module. Additionally, +if set in a file, {\rm\sl option} is set to {\rm\sl value} when the file is +{\tt Require}-d. +\end{Variants} + +\subsection[\tt Unset {\rm\sl option}.]{\tt Unset {\rm\sl option}.\comindex{Unset}} +This command resets {\rm\sl option} to its default value. + +\begin{Variants} +\item {\tt Local Unset {\rm\sl option}.\comindex{Local Unset}}\\ +This command resets {\rm\sl option} to its default value. The original state of {\rm\sl option} +is restored when the current \emph{section} ends. +\item {\tt Global Unset {\rm\sl option}.\comindex{Global Unset}}\\ +This command resets {\rm\sl option} to its default value. The original state of +{\rm\sl option} is \emph{not} restored at the end of the module. Additionally, +if unset in a file, {\rm\sl option} is reset to its default value when the file is +{\tt Require}-d. +\end{Variants} + \subsection[\tt Test {\rm\sl option}.]{\tt Test {\rm\sl option}.\comindex{Test}} This command prints the current value of {\rm\sl option}. +\subsection{Tables} +The general commands for tables are {\tt Add {\rm\sf table} {\rm\sl + value}}, {\tt Remove {\rm\sf table} {\rm\sl value}}, {\tt Test + {\rm\sf table}}, {\tt Test {\rm\sf table} for {\rm\sl value}} and + {\tt Print Table {\rm\sf table}}. + +\subsection[\tt Print Options.]{\tt Print Options.\comindex{Print Options}} +This command lists all available flags, options and tables. + \begin{Variants} -\item {\tt Test {\rm\sl flag}.}\\ -This command prints whether {\rm\sl flag} is on or off. +\item {\tt Print Tables}.\comindex{Print Tables}\\ +This is a synonymous of {\tt Print Options.} \end{Variants} \section{Requests to the environment} @@ -933,6 +971,7 @@ This command turns the normal display on. \subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\comindex{Set Printing Width}} +\label{SetPrintingWidth} This command sets which left-aligned part of the width of the screen is used for display. diff -Nru coq-doc-8.4pl2/doc/refman/RefMan-pre.tex coq-doc-8.4pl4/doc/refman/RefMan-pre.tex --- coq-doc-8.4pl2/doc/refman/RefMan-pre.tex 2012-08-07 22:47:51.000000000 +0000 +++ coq-doc-8.4pl4/doc/refman/RefMan-pre.tex 2014-04-24 15:13:03.000000000 +0000 @@ -938,7 +938,7 @@ % Integration of ZArith lemmas from Sophia and Nijmegen. -% $Id: RefMan-pre.tex 15698 2012-08-07 22:47:51Z herbelin $ +% $Id$ %%% Local Variables: %%% mode: latex diff -Nru coq-doc-8.4pl2/doc/refman/RefMan-tac.tex coq-doc-8.4pl4/doc/refman/RefMan-tac.tex --- coq-doc-8.4pl2/doc/refman/RefMan-tac.tex 2012-10-23 09:40:12.000000000 +0000 +++ coq-doc-8.4pl4/doc/refman/RefMan-tac.tex 2014-04-24 15:13:03.000000000 +0000 @@ -1890,7 +1890,7 @@ \tacindex{functional induction} \label{FunInduction} -The \emph{experimental} tactic \texttt{functional induction} performs +The tactic \texttt{functional induction} performs case analysis and induction following the definition of a function. It makes use of a principle generated by \texttt{Function} (see Section~\ref{Function}) or \texttt{Functional Scheme} @@ -2009,7 +2009,7 @@ This behaves like {\tt discriminate {\ident}} if {\ident} is the name of an hypothesis to which {\tt discriminate} is applicable; if the current goal is of the form {\term$_1$} {\tt <>} {\term$_2$}, - this behaves as {\tt intro {\ident}; injection {\ident}}. + this behaves as {\tt intro {\ident}; discriminate {\ident}}. \ErrMsg \errindex{No discriminable equalities} \end{Variants} @@ -3546,7 +3546,7 @@ generalize X1, X2; decide equality : eqdec. Goal forall a b:list (nat * nat), {a = b} + {a <> b}. -info auto with eqdec. +info_auto with eqdec. \end{coq_example} \begin{coq_eval} Abort. @@ -4191,8 +4191,9 @@ \label{inversion}} \subsection[\tt functional inversion \ident]{\tt functional inversion \ident\label{sec:functional-inversion}} +\tacindex{functional inversion} -\texttt{functional inversion} is a \emph{highly} experimental tactic +\texttt{functional inversion} is a tactic which performs inversion on hypothesis \ident\ of the form \texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ = \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been diff -Nru coq-doc-8.4pl2/ide/command_windows.ml coq-doc-8.4pl4/ide/command_windows.ml --- coq-doc-8.4pl2/ide/command_windows.ml 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/ide/command_windows.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ("Error while interpreting "^phrase^":\n"^str) | Interface.Good results -> diff -Nru coq-doc-8.4pl2/ide/command_windows.mli coq-doc-8.4pl4/ide/command_windows.mli --- coq-doc-8.4pl2/ide/command_windows.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/ide/command_windows.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* sync display_error (l,str); None | Interface.Good msg -> sync display_output msg; Some Safe - (* TODO: Restore someday the access to Decl_mode.get_damon_flag, - and also detect the use of admit, and then return Unsafe *) with | End_of_file -> (* Coqtop has died, let's trigger a reset_initial. *) raise RestartCoqtop @@ -890,9 +888,10 @@ end in try - match Coq.interp !mycoqtop ~raw:true ~verbose:false phrase with + match Coq.interp !mycoqtop ~raw:true ~verbose:false 0 phrase with | Interface.Fail (_, err) -> sync display_error err - | Interface.Good msg -> sync self#insert_message msg + | Interface.Good msg -> + sync self#insert_message msg with | End_of_file -> raise RestartCoqtop | e -> sync display_error (Printexc.to_string e) @@ -1256,7 +1255,7 @@ | Interface.Good true -> () | Interface.Good false -> let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in - match Coq.interp ct cmd with + match Coq.interp ct 0 cmd with | Interface.Fail (l,str) -> self#set_message ("Couln't add loadpath:\n"^str) | Interface.Good _ -> () diff -Nru coq-doc-8.4pl2/ide/coqide.mli coq-doc-8.4pl4/ide/coqide.mli --- coq-doc-8.4pl2/ide/coqide.mli 2012-12-03 17:32:11.000000000 +0000 +++ coq-doc-8.4pl4/ide/coqide.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] @@ -270,13 +276,13 @@ let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in (Ide_intf.to_answer xml c : 'a Interface.value) -let interp coqtop ?(raw=false) ?(verbose=true) s = - eval_call coqtop (Ide_intf.interp (raw,verbose,s)) +let interp coqtop ?(raw=false) ?(verbose=true) i s = + eval_call coqtop (Ide_intf.interp (i,raw,verbose,s)) let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i) let inloadpath coqtop s = eval_call coqtop (Ide_intf.inloadpath s) let mkcases coqtop s = eval_call coqtop (Ide_intf.mkcases s) -let status coqtop = eval_call coqtop Ide_intf.status -let hints coqtop = eval_call coqtop Ide_intf.hints +let status coqtop = eval_call coqtop (Ide_intf.status ()) +let hints coqtop = eval_call coqtop (Ide_intf.hints ()) module PrintOpt = struct @@ -308,8 +314,8 @@ let goals coqtop = let () = PrintOpt.enforce_hack coqtop in - eval_call coqtop Ide_intf.goals + eval_call coqtop (Ide_intf.goals ()) let evars coqtop = let () = PrintOpt.enforce_hack coqtop in - eval_call coqtop Ide_intf.evars + eval_call coqtop (Ide_intf.evars ()) diff -Nru coq-doc-8.4pl2/ide/coq.mli coq-doc-8.4pl4/ide/coq.mli --- coq-doc-8.4pl2/ide/coq.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/ide/coq.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ?raw:bool -> ?verbose:bool -> string -> string Interface.value + coqtop -> ?raw:bool -> ?verbose:bool -> int -> string -> string Interface.value val rewind : coqtop -> int -> int Interface.value val status : coqtop -> Interface.status Interface.value val goals : coqtop -> Interface.goals option Interface.value diff -Nru coq-doc-8.4pl2/ide/gtk_parsing.ml coq-doc-8.4pl4/ide/gtk_parsing.ml --- coq-doc-8.4pl2/ide/gtk_parsing.ml 2013-02-05 14:42:44.000000000 +0000 +++ coq-doc-8.4pl4/ide/gtk_parsing.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* n then - user_err_loc (loc,"",str "Projection has not the right number of explicit parameters."); + user_err_loc (loc,"",str "Projection does not have the right number of explicit parameters."); with Not_found -> user_err_loc (loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection.")) diff -Nru coq-doc-8.4pl2/interp/constrintern.mli coq-doc-8.4pl4/interp/constrintern.mli --- coq-doc-8.4pl2/interp/constrintern.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/interp/constrintern.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (open_constr_expr,rlevel) abstract_argument_type -val globwit_open_constr_gen : bool -> (open_glob_constr,glevel) abstract_argument_type -val wit_open_constr_gen : bool -> (open_constr,tlevel) abstract_argument_type +val rawwit_open_constr_gen : bool * bool -> (open_constr_expr,rlevel) abstract_argument_type +val globwit_open_constr_gen : bool * bool -> (open_glob_constr,glevel) abstract_argument_type +val wit_open_constr_gen : bool * bool -> (open_constr,tlevel) abstract_argument_type val rawwit_open_constr : (open_constr_expr,rlevel) abstract_argument_type val globwit_open_constr : (open_glob_constr,glevel) abstract_argument_type @@ -195,6 +195,10 @@ val globwit_casted_open_constr : (open_glob_constr,glevel) abstract_argument_type val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type +val rawwit_open_constr_wTC : (open_constr_expr,rlevel) abstract_argument_type +val globwit_open_constr_wTC : (open_glob_constr,glevel) abstract_argument_type +val wit_open_constr_wTC : (open_constr,tlevel) abstract_argument_type + val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type val globwit_constr_with_bindings : (glob_constr_and_expr with_bindings,glevel) abstract_argument_type val wit_constr_with_bindings : (constr with_bindings sigma,tlevel) abstract_argument_type @@ -280,7 +284,7 @@ | ConstrArgType | ConstrMayEvalArgType | QuantHypArgType - | OpenConstrArgType of bool + | OpenConstrArgType of bool * bool | ConstrWithBindingsArgType | BindingsArgType | RedExprArgType diff -Nru coq-doc-8.4pl2/interp/implicit_quantifiers.ml coq-doc-8.4pl4/interp/implicit_quantifiers.ml --- coq-doc-8.4pl2/interp/implicit_quantifiers.ml 2013-03-18 14:09:52.000000000 +0000 +++ coq-doc-8.4pl4/interp/implicit_quantifiers.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - Pp.warning "Capture check in multiple binders not done"; acc + Pp.msg_warn "Capture check in multiple binders not done"; acc let free_vars_of_constr_expr c = let rec aux bdvars l = function diff -Nru coq-doc-8.4pl2/interp/topconstr.mli coq-doc-8.4pl4/interp/topconstr.mli --- coq-doc-8.4pl2/interp/topconstr.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/interp/topconstr.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let sign, s = dest_arity env full_arity in + let sign, s = + try dest_arity env full_arity + with NotArity -> raise (InductiveError (NotAnArity (env, full_arity))) + in let status,cst = match s with | Type u when ar_level <> None (* Explicitly polymorphic *) && no_upper_constraints u cst -> diff -Nru coq-doc-8.4pl2/kernel/indtypes.mli coq-doc-8.4pl4/kernel/indtypes.mli --- coq-doc-8.4pl2/kernel/indtypes.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/kernel/indtypes.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* raise (LocalArity None) in srec (push_rel (na1,None,a1) env) t ar' (union_constraints u univ) - | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *) - let ksort = match kind_of_term (whd_betadeltaiota env a2) with - | Sort s -> family_of_sort s - | _ -> raise (LocalArity None) in - let dep_ind = build_dependent_inductive ind specif params in - let univ = - try conv env a1 dep_ind - with NotConvertible -> raise (LocalArity None) in - check_allowed_sort ksort specif; - union_constraints u univ + (* The last Prod domain is the type of the scrutinee *) + | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) + let env' = push_rel (na1,None,a1) env in + let ksort = match kind_of_term (whd_betadeltaiota env' a2) with + | Sort s -> family_of_sort s + | _ -> raise (LocalArity None) in + let dep_ind = build_dependent_inductive ind specif params in + let univ = + try conv env a1 dep_ind + with NotConvertible -> raise (LocalArity None) in + check_allowed_sort ksort specif; + union_constraints u univ | _, (_,Some _,_ as d)::ar' -> - srec (push_rel d env) (lift 1 pt') ar' u + srec (push_rel d env) (lift 1 pt') ar' u | _ -> raise (LocalArity None) in @@ -895,12 +897,12 @@ raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) | CoFix (j,(_,varit,vdefs as recdef)) -> - if (List.for_all (noccur_with_meta n nbfix) args) + if List.for_all (noccur_with_meta n nbfix) args then - let nbfix = Array.length vdefs in - if (array_for_all (noccur_with_meta n nbfix) varit) then + if array_for_all (noccur_with_meta n nbfix) varit then + let nbfix = Array.length vdefs in let env' = push_rec_types recdef env in - (Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs; + (Array.iter (check_rec_call env' alreadygrd (n+nbfix) vlra) vdefs; List.iter (check_rec_call env alreadygrd n vlra) args) else raise (CoFixGuardError (env,RecCallInTypeOfDef c)) diff -Nru coq-doc-8.4pl2/kernel/inductive.mli coq-doc-8.4pl4/kernel/inductive.mli --- coq-doc-8.4pl2/kernel/inductive.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/kernel/inductive.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* full_add_module mb env) diff -Nru coq-doc-8.4pl2/kernel/safe_typing.mli coq-doc-8.4pl4/kernel/safe_typing.mli --- coq-doc-8.4pl2/kernel/safe_typing.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/kernel/safe_typing.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* true - | Max ([UniverseLevel.Set], []) -> warning "Non canonical Set"; true + | Max ([UniverseLevel.Set], []) -> msg_warn "Non canonical Set"; true | u -> false let is_univ_variable = function diff -Nru coq-doc-8.4pl2/kernel/univ.mli coq-doc-8.4pl4/kernel/univ.mli --- coq-doc-8.4pl2/kernel/univ.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/kernel/univ.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* coqlib | None -> coqroot in - if Sys.file_exists (Filename.concat coqlib file) + if Sys.file_exists (coqlib//file) then coqlib else Util.error "cannot guess a path for Coq libraries; please use -coqlib option") @@ -54,18 +56,14 @@ Util.split_string_at sep p let xdg_data_home = - Filename.concat - (System.getenv_else "XDG_DATA_HOME" (Filename.concat System.home ".local/share")) - "coq" + (System.getenv_else "XDG_DATA_HOME" (System.home//".local/share"))//"coq" let xdg_config_home = - Filename.concat - (System.getenv_else "XDG_CONFIG_HOME" (Filename.concat System.home ".config")) - "coq" + (System.getenv_else "XDG_CONFIG_HOME" (System.home//".config"))//"coq" let xdg_data_dirs = (try - List.map (fun dir -> Filename.concat dir "coq") (path_to_list (Sys.getenv "XDG_DATA_DIRS")) + List.map (fun dir -> dir//"coq") (path_to_list (Sys.getenv "XDG_DATA_DIRS")) with Not_found -> ["/usr/local/share/coq";"/usr/share/coq"]) @ (match Coq_config.datadir with |None -> [] |Some datadir -> [datadir]) @@ -84,7 +82,7 @@ match l with | [] -> raise Not_found | p :: tl -> - if Sys.file_exists (Filename.concat p f) + if Sys.file_exists (p//f) then p else which tl f @@ -108,7 +106,7 @@ then Coq_config.camllib else let camlbin = camlbin () in - let com = (Filename.concat camlbin "ocamlc") ^ " -where" in + let com = (camlbin//"ocamlc") ^ " -where" in let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in Util.strip res @@ -117,7 +115,7 @@ if !Flags.boot then Coq_config.camlp4bin else try guess_camlp4bin () with e when e <> Sys.Break -> let cb = camlbin () in - if Sys.file_exists (Filename.concat cb (exe Coq_config.camlp4)) then cb + if Sys.file_exists (cb//(exe Coq_config.camlp4)) then cb else Coq_config.camlp4bin let camlp4lib () = @@ -125,7 +123,7 @@ then Coq_config.camlp4lib else let camlp4bin = camlp4bin () in - let com = (Filename.concat camlp4bin Coq_config.camlp4) ^ " -where" in + let com = (camlp4bin//Coq_config.camlp4) ^ " -where" in let ex,res = System.run_command (fun x -> x) (fun _ -> ()) com in match ex with |Unix.WEXITED 0 -> Util.strip res diff -Nru coq-doc-8.4pl2/lib/envars.mli coq-doc-8.4pl4/lib/envars.mli --- coq-doc-8.4pl2/lib/envars.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/lib/envars.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit val msgerrnl : std_ppcmds -> unit val msg_warning : std_ppcmds -> unit +val msg_warn : string -> unit (** Same specific display in emacs as warning, but without the "Warning:" **) val msg_debug : std_ppcmds -> unit diff -Nru coq-doc-8.4pl2/lib/profile.ml coq-doc-8.4pl4/lib/profile.ml --- coq-doc-8.4pl2/lib/profile.ml 2013-03-18 14:09:52.000000000 +0000 +++ coq-doc-8.4pl4/lib/profile.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise reraise + msg_warn ("Removed file "^f'); close_out ch; Sys.remove f'; raise reraise (************************************************************************) (*s Display the memory use of a library. *) diff -Nru coq-doc-8.4pl2/library/library.mli coq-doc-8.4pl4/library/library.mli --- coq-doc-8.4pl2/library/library.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/library/library.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <:expr< Genarg.rawwit_constr_may_eval >> | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >> | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >> - | OpenConstrArgType b -> <:expr< Genarg.rawwit_open_constr_gen $mlexpr_of_bool b$ >> + | OpenConstrArgType (b1,b2) -> <:expr< Genarg.rawwit_open_constr_gen ($mlexpr_of_bool b1$,$mlexpr_of_bool b2$) >> | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.rawwit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >> @@ -62,7 +62,7 @@ | ConstrArgType -> <:expr< Genarg.globwit_constr >> | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >> | RedExprArgType -> <:expr< Genarg.globwit_red_expr >> - | OpenConstrArgType b -> <:expr< Genarg.globwit_open_constr_gen $mlexpr_of_bool b$ >> + | OpenConstrArgType (b1,b2) -> <:expr< Genarg.globwit_open_constr_gen ($mlexpr_of_bool b1$,$mlexpr_of_bool b2$) >> | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.globwit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >> @@ -92,7 +92,7 @@ | ConstrArgType -> <:expr< Genarg.wit_constr >> | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >> | RedExprArgType -> <:expr< Genarg.wit_red_expr >> - | OpenConstrArgType b -> <:expr< Genarg.wit_open_constr_gen $mlexpr_of_bool b$ >> + | OpenConstrArgType (b1,b2) -> <:expr< Genarg.wit_open_constr_gen ($mlexpr_of_bool b1$,$mlexpr_of_bool b2$) >> | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.wit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >> diff -Nru coq-doc-8.4pl2/parsing/egrammar.ml coq-doc-8.4pl4/parsing/egrammar.ml --- coq-doc-8.4pl2/parsing/egrammar.ml 2013-03-18 14:09:52.000000000 +0000 +++ coq-doc-8.4pl4/parsing/egrammar.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ((),c) ] ] ; + open_constr_wTC: + [ [ c = constr -> ((),c) ] ] + ; casted_open_constr: [ [ c = constr -> ((),c) ] ] ; diff -Nru coq-doc-8.4pl2/parsing/g_vernac.ml4 coq-doc-8.4pl4/parsing/g_vernac.ml4 --- coq-doc-8.4pl2/parsing/g_vernac.ml4 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/parsing/g_vernac.ml4 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) - | IDENT "Include"; e = module_expr_inl; l = LIST0 ext_module_expr -> + | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr -> VernacInclude(e::l) | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> Flags.if_verbose @@ -842,6 +842,7 @@ -> PrintCoercionPaths (s,t) | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions | IDENT "Tables" -> PrintTables + | IDENT "Options" -> PrintTables (* A Synonymous to Tables *) | IDENT "Hint" -> PrintHintGoal | IDENT "Hint"; qid = smart_global -> PrintHint qid | IDENT "Hint"; "*" -> PrintHintDb diff -Nru coq-doc-8.4pl2/parsing/g_xml.ml4 coq-doc-8.4pl4/parsing/g_xml.ml4 --- coq-doc-8.4pl2/parsing/g_xml.ml4 2013-03-18 14:09:52.000000000 +0000 +++ coq-doc-8.4pl4/parsing/g_xml.ml4 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Gram.entry table *) (* Typically for tactic user extensions *) let open_constr = - make_gen_entry utactic (rawwit_open_constr_gen false) "open_constr" + make_gen_entry utactic (rawwit_open_constr_gen (false,false)) "open_constr" let casted_open_constr = - make_gen_entry utactic (rawwit_open_constr_gen true) "casted_open_constr" + make_gen_entry utactic (rawwit_open_constr_gen (true,false)) "casted_open_constr" + let open_constr_wTC = + make_gen_entry utactic (rawwit_open_constr_gen (false,true)) "open_constr_wTC" let constr_with_bindings = make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings" let bindings = diff -Nru coq-doc-8.4pl2/parsing/pcoq.mli coq-doc-8.4pl4/parsing/pcoq.mli --- coq-doc-8.4pl2/parsing/pcoq.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/parsing/pcoq.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat) (out_gen rawwit_red_expr x) - | OpenConstrArgType b -> prc (snd (out_gen (rawwit_open_constr_gen b) x)) + | OpenConstrArgType (b1,b2) -> prc (snd (out_gen (rawwit_open_constr_gen (b1,b2)) x)) | ConstrWithBindingsArgType -> pr_with_bindings prc prlc (out_gen rawwit_constr_with_bindings x) | BindingsArgType -> @@ -195,7 +195,7 @@ pr_red_expr (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat) (out_gen globwit_red_expr x) - | OpenConstrArgType b -> prc (snd (out_gen (globwit_open_constr_gen b) x)) + | OpenConstrArgType (b1,b2) -> prc (snd (out_gen (globwit_open_constr_gen (b1,b2)) x)) | ConstrWithBindingsArgType -> pr_with_bindings prc prlc (out_gen globwit_constr_with_bindings x) | BindingsArgType -> @@ -236,7 +236,7 @@ | RedExprArgType -> pr_red_expr (prc,prlc,pr_evaluable_reference,prpat) (out_gen wit_red_expr x) - | OpenConstrArgType b -> prc (snd (out_gen (wit_open_constr_gen b) x)) + | OpenConstrArgType (b1,b2) -> prc (snd (out_gen (wit_open_constr_gen (b1,b2)) x)) | ConstrWithBindingsArgType -> let (c,b) = (out_gen wit_constr_with_bindings x).Evd.it in pr_with_bindings prc prlc (c,b) diff -Nru coq-doc-8.4pl2/parsing/pptactic.mli coq-doc-8.4pl4/parsing/pptactic.mli --- coq-doc-8.4pl2/parsing/pptactic.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/parsing/pptactic.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (mt ()) | Some c -> (* Force evaluation *) - let pb = pr_lconstr_env env c in + let pb = pr_lconstr_core true env c in let pb = if isCast c then surround pb else pb in (str" := " ++ pb ++ cut () ) in - let pt = pr_ltype_env env typ in + let pt = pr_ltype_core true env typ in let ptyp = (str" : " ++ pt) in (pr_id id ++ hov 0 (pbody ++ ptyp)) @@ -217,10 +217,10 @@ | None -> mt () | Some c -> (* Force evaluation *) - let pb = pr_lconstr_env env c in + let pb = pr_lconstr_core true env c in let pb = if isCast c then surround pb else pb in (str":=" ++ spc () ++ pb ++ spc ()) in - let ptyp = pr_ltype_env env typ in + let ptyp = pr_ltype_core true env typ in match na with | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) @@ -571,7 +571,7 @@ (str"fix " ++ pr_id f ++ str"/" ++ int n) | FixRule (f,n,others,j) -> - if j<>0 then warning "Unsupported printing of \"fix\""; + if j<>0 then msg_warn "Unsupported printing of \"fix\""; let rec print_mut = function | (f,n,ar)::oth -> pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth @@ -583,7 +583,7 @@ (str"cofix " ++ pr_id f) | Cofix (f,others,j) -> - if j<>0 then warning "Unsupported printing of \"fix\""; + if j<>0 then msg_warn "Unsupported printing of \"fix\""; let rec print_mut = function | (f,ar)::oth -> (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth) diff -Nru coq-doc-8.4pl2/parsing/printer.mli coq-doc-8.4pl4/parsing/printer.mli --- coq-doc-8.4pl2/parsing/printer.mli 2013-03-21 21:19:32.000000000 +0000 +++ coq-doc-8.4pl4/parsing/printer.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <:expr< Genarg.VarArgType >> | Genarg.StringArgType -> <:expr< Genarg.StringArgType >> | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> - | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >> + | Genarg.OpenConstrArgType (b1,b2) -> <:expr< Genarg.OpenConstrArgType ($mlexpr_of_bool b1$, $mlexpr_of_bool b2$) >> | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >> | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >> diff -Nru coq-doc-8.4pl2/parsing/q_util.ml4 coq-doc-8.4pl4/parsing/q_util.ml4 --- coq-doc-8.4pl2/parsing/q_util.ml4 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/parsing/q_util.ml4 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (t, l) | Construct _ -> (t,l) @@ -576,7 +576,7 @@ onLastHypId (fun heq_id -> tclTHENLIST [ (* Then the new hypothesis *) tclMAP introduction_no_check dyn_infos.rec_hyps; - (* observe_tac "after_introduction" *)(fun g' -> + observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) let new_term_value_eq = pf_type_of g' (mkVar heq_id) in (* compute the new value of the body *) @@ -603,7 +603,7 @@ } in clean_goal_with_heq ptes_infos continue_tac new_infos g' - )]) + )]) ] g diff -Nru coq-doc-8.4pl2/plugins/funind/g_indfun.ml4 coq-doc-8.4pl4/plugins/funind/g_indfun.ml4 --- coq-doc-8.4pl2/plugins/funind/g_indfun.ml4 2013-03-18 14:09:52.000000000 +0000 +++ coq-doc-8.4pl4/plugins/funind/g_indfun.ml4 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* + match pat with + | Genarg.IntroIdentifier id -> add id acc + | _ -> anomaly "Not an identifier" + ) + (List.nth intro_pats (pred i)) + empty + in let prove_branche i g = (* We get the identifiers of this branch *) - let this_branche_ids = - List.fold_right - (fun (_,pat) acc -> - match pat with - | Genarg.IntroIdentifier id -> Idset.add id acc - | _ -> anomaly "Not an identifier" - ) - (List.nth intro_pats (pred i)) - Idset.empty - in (* and get the real args of the branch by unfolding the defined constant *) let pre_args,pre_tac = List.fold_right (fun (id,b,t) (pre_args,pre_tac) -> - if Idset.mem id this_branche_ids + if Idset.mem id (this_branche_ids Idset.empty Idset.add i) then match b with - | None -> (id::pre_args,pre_tac) + | None -> + (id::pre_args,pre_tac) | Some b -> (pre_args, tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac @@ -347,8 +351,8 @@ when (eq_constr eq eq_ind) && array_exists (eq_constr graph') graphs_constr -> - ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) - ::args.(2)::acc) + ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) + ::args.(2)::acc) | _ -> mkVar hid :: acc end | _ -> mkVar hid :: acc @@ -390,7 +394,7 @@ | [res;hres] -> res,hres | _ -> assert false in - observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor); + observe_tac_msg (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor) ( tclTHENSEQ [ @@ -455,11 +459,10 @@ fun g -> observe (pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g)) (mkVar principle_id,bindings)); - functional_induction false (applist(funs_constr.(i),List.map mkVar args_names)) - (Some (mkVar principle_id,bindings)) - pat g + h_apply false false [dummy_loc,(mkVar principle_id,bindings)] g )) - (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) + (fun i g -> observe_tac ("proving branche "^string_of_int i) + (tclTHEN (tclMAP h_intro (this_branche_ids [] (fun a b -> a::b) i)) (prove_branche i)) g ) ] g diff -Nru coq-doc-8.4pl2/plugins/funind/merge.ml coq-doc-8.4pl4/plugins/funind/merge.ml --- coq-doc-8.4pl2/plugins/funind/merge.ml 2013-03-18 14:09:52.000000000 +0000 +++ coq-doc-8.4pl4/plugins/funind/merge.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* let (f,_) = decompose_app t in eq_constr f (well_founded ()) - | _ -> assert false + | _ -> false in let compare t1 t2 = let b1,b2= is_well_founded t1,is_well_founded t2 in diff -Nru coq-doc-8.4pl2/plugins/funind/Recdef.v coq-doc-8.4pl4/plugins/funind/Recdef.v --- coq-doc-8.4pl2/plugins/funind/Recdef.v 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/plugins/funind/Recdef.v 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* = 8.5, this option is set by default. +*) + let read f () = !f let write f x = f:=x @@ -81,6 +98,14 @@ optread = read old_style_flag; optwrite = write old_style_flag } +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "Omega automatic reset of generated names"; + optkey = ["Stable";"Omega"]; + optread = read reset_flag; + optwrite = write reset_flag } let all_time = timing "Omega " let solver_time = timing "Solver " @@ -89,30 +114,35 @@ let simpl_time = timing "Simpl " let generalize_time = timing "Generalize" +let intref, reset_all_references = + let refs = ref [] in + (fun n -> let r = ref n in refs := (r,n) :: !refs; r), + (fun () -> List.iter (fun (r,n) -> r:=n) !refs) + let new_identifier = - let cpt = ref 0 in + let cpt = intref 0 in (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; id_of_string s) let new_identifier_state = - let cpt = ref 0 in + let cpt = intref 0 in (fun () -> let s = make_ident "State" (Some !cpt) in incr cpt; s) let new_identifier_var = - let cpt = ref 0 in + let cpt = intref 0 in (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; id_of_string s) let new_id = - let cpt = ref 0 in fun () -> incr cpt; !cpt + let cpt = intref 0 in fun () -> incr cpt; !cpt let new_var_num = - let cpt = ref 1000 in (fun () -> incr cpt; !cpt) + let cpt = intref 1000 in (fun () -> incr cpt; !cpt) let new_var = - let cpt = ref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt) + let cpt = intref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt) let display_var i = Printf.sprintf "X%d" i -let intern_id,unintern_id = +let intern_id,unintern_id,reset_intern_tables = let cpt = ref 0 in let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in (fun (name : identifier) -> @@ -124,7 +154,8 @@ (fun idx -> try Hashtbl.find co_table idx with Not_found -> let v = new_var () in - Hashtbl.add table v idx; Hashtbl.add co_table idx v; v) + Hashtbl.add table v idx; Hashtbl.add co_table idx v; v), + (fun () -> cpt := 0; Hashtbl.clear table) let mk_then = tclTHENLIST @@ -141,19 +172,28 @@ in loop -let tag_hypothesis,tag_of_hyp, hyp_of_tag = +let tag_hypothesis,tag_of_hyp, hyp_of_tag, clear_tags = let l = ref ([]:(identifier * int) list) in (fun h id -> l := (h,id):: !l), (fun h -> try List.assoc h !l with Not_found -> failwith "tag_hypothesis"), - (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis") + (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis"), + (fun () -> l := []) -let hide_constr,find_constr,clear_tables,dump_tables = +let hide_constr,find_constr,clear_constr_tables,dump_tables = let l = ref ([]:(constr * (identifier * identifier * bool)) list) in (fun h id eg b -> l := (h,(id,eg,b)):: !l), (fun h -> try list_assoc_f eq_constr h !l with Not_found -> failwith "find_contr"), (fun () -> l := []), (fun () -> !l) +let reset_all () = + if !reset_flag then begin + reset_all_references (); + reset_intern_tables (); + clear_tags (); + clear_constr_tables () + end + (* Lazy evaluation is used for Coq constants, because this code is evaluated before the compiled modules are loaded. To use the constant Zplus, one must type "Lazy.force coq_Zplus" @@ -1388,7 +1428,7 @@ tclTHEN (tclTRY (clear [id])) (intro_using id) let coq_omega gl = - clear_tables (); + clear_constr_tables (); let tactic_normalisation, system = List.fold_left (destructure_omega gl) ([],[]) (pf_hyps_types gl) in let prelude,sys = @@ -1814,6 +1854,7 @@ let omega_solver gl = Coqlib.check_required_library ["Coq";"omega";"Omega"]; + reset_all (); let result = destructure_goal gl in (* if !display_time_flag then begin text_time (); flush Pervasives.stdout end; *) diff -Nru coq-doc-8.4pl2/plugins/omega/g_omega.ml4 coq-doc-8.4pl4/plugins/omega/g_omega.ml4 --- coq-doc-8.4pl2/plugins/omega/g_omega.ml4 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/plugins/omega/g_omega.ml4 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Fcons a (Fapp l1 m) end. -Lemma fcons_correct : forall l l1, - PCond l (Fapp l1 nil) -> PCond l l1. -induction l1; simpl; intros. - trivial. - elim PCond_fcons_inv with (1 := H); intros. - destruct l1; auto. -Qed. + Lemma fcons_correct : forall l l1, + (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1. + Proof. + intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1. + induction l1; simpl; intros. + trivial. + elim PCond_fcons_inv with (1 := H); intros. + destruct l1; trivial. split; trivial. apply IHl1; trivial. + Qed. End Fcons_impl. diff -Nru coq-doc-8.4pl2/plugins/setoid_ring/Field.v coq-doc-8.4pl4/plugins/setoid_ring/Field.v --- coq-doc-8.4pl2/plugins/setoid_ring/Field.v 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/plugins/setoid_ring/Field.v 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in + let (evd',j) = Coercion.inh_conv_coerce_to true loc env !isevars j p in isevars := evd'; j | None -> j diff -Nru coq-doc-8.4pl2/plugins/subtac/subtac_cases.mli coq-doc-8.4pl4/plugins/subtac/subtac_cases.mli --- coq-doc-8.4pl2/plugins/subtac/subtac_cases.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/plugins/subtac/subtac_cases.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* anomaly "apply_coercion" - let inh_app_fun env isevars j = + let inh_app_fun _ env isevars j = let isevars = ref isevars in let t = hnf env !isevars j.uj_type in match kind_of_term t with @@ -481,8 +481,8 @@ | Some (init, cur) -> (evd, cj) - let inh_conv_coerce_to = inh_conv_coerce_to_gen false - let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true + let inh_conv_coerce_to _ = inh_conv_coerce_to_gen false + let inh_conv_coerce_rigid_to _ = inh_conv_coerce_to_gen true let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) = let nabsinit, nabs = diff -Nru coq-doc-8.4pl2/plugins/subtac/subtac.ml coq-doc-8.4pl4/plugins/subtac/subtac.ml --- coq-doc-8.4pl2/plugins/subtac/subtac.ml 2013-03-18 14:09:52.000000000 +0000 +++ coq-doc-8.4pl4/plugins/subtac/subtac.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (fun _ -> true) - | Some s -> (fun i -> Intset.mem i s) + | Some s -> set := s; + (fun i -> Intset.mem i !set) in let _ = Array.iteri (fun i x -> - if p i && solve_obligation_by_tac prg obls' i tac then - decr rem) + if p i && solve_obligation_by_tac prg obls' i tac then + let deps = dependencies obls i in + (set := Intset.union !set deps; + decr rem)) obls' in update_obls prg obls' !rem diff -Nru coq-doc-8.4pl2/plugins/subtac/subtac_pretyping_F.ml coq-doc-8.4pl4/plugins/subtac/subtac_pretyping_F.ml --- coq-doc-8.4pl2/plugins/subtac/subtac_pretyping_F.ml 2013-03-18 14:09:52.000000000 +0000 +++ coq-doc-8.4pl4/plugins/subtac/subtac_pretyping_F.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* j - | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t + | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t let push_rels vars env = List.fold_right push_rel vars env @@ -188,11 +188,14 @@ (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [( evdref)] and *) (* the type constraint tycon *) - let rec pretype (tycon : type_constraint) env evdref lvar c = + let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar c = (* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_glob_constr env c ++ *) (* str " with tycon " ++ Evarutil.pr_tycon env tycon) *) (* with _ -> () *) (* in *) + let pretype = pretype resolve_tc in + let pretype_type = pretype_type resolve_tc in + let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in match c with | GRef (loc,ref) -> inh_conv_coerce_to_tycon loc env evdref @@ -335,7 +338,7 @@ | [] -> resj | c::rest -> let argloc = loc_of_glob_constr c in - let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in + let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in let resty = whd_betadeltaiota env !evdref resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> @@ -557,7 +560,7 @@ inh_conv_coerce_to_tycon loc env evdref cj tycon (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) - and pretype_type valcon env evdref lvar = function + and pretype_type resolve_tc valcon env evdref lvar = function | GHole loc -> (match valcon with | Some v -> @@ -577,7 +580,7 @@ { utj_val = e_new_evar evdref env ~src:loc (mkSort s); utj_type = s}) | c -> - let j = pretype empty_tycon env evdref lvar c in + let j = pretype resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in match valcon with @@ -592,9 +595,9 @@ let c' = match kind with | OfType exptyp -> let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in - (pretype tycon env evdref lvar c).uj_val + (pretype resolve_classes tycon env evdref lvar c).uj_val | IsType -> - (pretype_type empty_valcon env evdref lvar c).utj_val + (pretype_type resolve_classes empty_valcon env evdref lvar c).utj_val in if resolve_classes then (try @@ -616,14 +619,14 @@ let understand_judgment sigma env c = let evdref = ref (create_evar_defs sigma) in - let j = pretype empty_tycon env evdref ([],[]) c in + let j = pretype true empty_tycon env evdref ([],[]) c in let evd = consider_remaining_unif_problems env !evdref in let j = j_nf_evar evd j in check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j let understand_judgment_tcc evdref env c = - let j = pretype empty_tycon env evdref ([],[]) c in + let j = pretype true empty_tycon env evdref ([],[]) c in j_nf_evar !evdref j (* Raw calls to the unsafe inference machine: boolean says if we must diff -Nru coq-doc-8.4pl2/plugins/subtac/subtac_pretyping.ml coq-doc-8.4pl4/plugins/subtac/subtac_pretyping.ml --- coq-doc-8.4pl2/plugins/subtac/subtac_pretyping.ml 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/plugins/subtac/subtac_pretyping.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Libnames.is_dirpath_prefix_of modul dirpath) modules with [] -> - Pp.warning ("Modules not supported: reference to "^ + Pp.msg_warn ("Modules not supported: reference to "^ Libnames.string_of_path path^" will be wrong"); dirpath | [modul] -> modul diff -Nru coq-doc-8.4pl2/plugins/xml/dumptree.ml4 coq-doc-8.4pl4/plugins/xml/dumptree.ml4 --- coq-doc-8.4pl2/plugins/xml/dumptree.ml4 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/plugins/xml/dumptree.ml4 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* "AXIOM","Declaration" | DK.IsAssumption DK.Logical -> "AXIOM","Axiom" | DK.IsAssumption DK.Conjectural -> - Pp.warning "Conjecture not supported in dtd (used Declaration instead)"; + Pp.msg_warn "Conjecture not supported in dtd (used Declaration instead)"; "AXIOM","Declaration" | DK.IsDefinition DK.Definition -> "DEFINITION","Definition" | DK.IsDefinition DK.Example -> - Pp.warning "Example not supported in dtd (used Definition instead)"; + Pp.msg_warn "Example not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Coercion -> - Pp.warning "Coercion not supported in dtd (used Definition instead)"; + Pp.msg_warn "Coercion not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.SubClass -> - Pp.warning "SubClass not supported in dtd (used Definition instead)"; + Pp.msg_warn "SubClass not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.CanonicalStructure -> - Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)"; + Pp.msg_warn "CanonicalStructure not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Fixpoint -> - Pp.warning "Fixpoint not supported in dtd (used Definition instead)"; + Pp.msg_warn "Fixpoint not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.CoFixpoint -> - Pp.warning "CoFixpoint not supported in dtd (used Definition instead)"; + Pp.msg_warn "CoFixpoint not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Scheme -> - Pp.warning "Scheme not supported in dtd (used Definition instead)"; + Pp.msg_warn "Scheme not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.StructureComponent -> - Pp.warning "StructureComponent not supported in dtd (used Definition instead)"; + Pp.msg_warn "StructureComponent not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.IdentityCoercion -> - Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)"; + Pp.msg_warn "IdentityCoercion not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Instance -> - Pp.warning "Instance not supported in dtd (used Definition instead)"; + Pp.msg_warn "Instance not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Method -> - Pp.warning "Method not supported in dtd (used Definition instead)"; + Pp.msg_warn "Method not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) -> "THEOREM",DK.string_of_theorem_kind thm | DK.IsProof _ -> - Pp.warning "Unsupported theorem kind (used Theorem instead)"; + Pp.msg_warn "Unsupported theorem kind (used Theorem instead)"; "THEOREM",DK.string_of_theorem_kind DK.Theorem ;; diff -Nru coq-doc-8.4pl2/pretyping/arguments_renaming.ml coq-doc-8.4pl4/pretyping/arguments_renaming.ml --- coq-doc-8.4pl2/pretyping/arguments_renaming.ml 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/pretyping/arguments_renaming.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] let discharge_rename_args = function - | _, (ReqGlobal (c, names), _) -> - let c' = pop_global_reference c in - let vars = section_segment_of_reference c in - let var_names = List.map (fun (id, _,_,_) -> Name id) vars in - let names' = List.map (fun l -> var_names @ l) names in - Some (ReqGlobal (c', names), (c', names')) + | _, (ReqGlobal (c, names), _ as req) -> + (try + let vars = section_segment_of_reference c in + let c' = pop_global_reference c in + let var_names = List.map (fun (id, _,_,_) -> Name id) vars in + let names' = List.map (fun l -> var_names @ l) names in + Some (ReqGlobal (c', names), (c', names')) + with Not_found -> Some req) | _ -> None let rebuild_rename_args x = x diff -Nru coq-doc-8.4pl2/pretyping/arguments_renaming.mli coq-doc-8.4pl4/pretyping/arguments_renaming.mli --- coq-doc-8.4pl2/pretyping/arguments_renaming.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/pretyping/arguments_renaming.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let (evd',j) = Coercion.inh_conv_coerce_to loc env !evdref j p in + let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j p in evdref := evd'; j | None -> j diff -Nru coq-doc-8.4pl2/pretyping/cases.mli coq-doc-8.4pl4/pretyping/cases.mli --- coq-doc-8.4pl2/pretyping/cases.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/pretyping/cases.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* evar_map -> unsafe_judgment -> evar_map * unsafe_judgment + bool -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment (* [inh_coerce_to_sort env evd j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as @@ -57,10 +57,10 @@ (* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and [j.uj_type] are convertible; it fails if no coercion is applicable *) - val inh_conv_coerce_to : loc -> + val inh_conv_coerce_to : bool -> loc -> env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment - val inh_conv_coerce_rigid_to : loc -> + val inh_conv_coerce_rigid_to : bool -> loc -> env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment (* [inh_conv_coerces_to loc env evd t t'] checks if an object of type [t] @@ -140,9 +140,11 @@ lookup_path_to_fun_from env evd j.uj_type in (evd,apply_coercion env evd p j t) - let inh_app_fun env evd j = + let inh_app_fun resolve_tc env evd j = try inh_app_fun env evd j - with Not_found -> + with + | Not_found when not resolve_tc -> (evd, j) + | Not_found -> try inh_app_fun env (saturate_evd env evd) j with Not_found -> (evd, j) @@ -221,13 +223,15 @@ | _ -> raise NoCoercion (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) - let inh_conv_coerce_to_gen rigidonly loc env evd cj (n, t) = + let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj (n, t) = match n with None -> let (evd', val') = try inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t - with NoCoercion -> + with + | NoCoercion when not resolve_tc -> error_actual_type_loc loc env evd cj t + | NoCoercion -> let evd = saturate_evd env evd in try inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t @@ -238,8 +242,8 @@ (evd',{ uj_val = val'; uj_type = t }) | Some (init, cur) -> (evd, cj) - let inh_conv_coerce_to = inh_conv_coerce_to_gen false - let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true + let inh_conv_coerce_to resolve_tc = inh_conv_coerce_to_gen resolve_tc false + let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true let inh_conv_coerces_to loc env (evd : evar_map) t (abs, t') = diff -Nru coq-doc-8.4pl2/pretyping/coercion.mli coq-doc-8.4pl4/pretyping/coercion.mli --- coq-doc-8.4pl2/pretyping/coercion.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/pretyping/coercion.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* evar_map -> unsafe_judgment -> evar_map * unsafe_judgment + bool -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as @@ -40,13 +42,15 @@ val inh_coerce_to_prod : loc -> env -> evar_map -> type_constraint_type -> evar_map * type_constraint_type - (** [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type + (** [inh_conv_coerce_to resolve_tc loc env isevars j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and - [j.uj_type] are convertible; it fails if no coercion is applicable *) - val inh_conv_coerce_to : loc -> + [j.uj_type] are convertible; it fails if no coercion is applicable. + resolve_tc=false disables resolving type classes (as the last + resort before failing) *) + val inh_conv_coerce_to : bool -> loc -> env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment - val inh_conv_coerce_rigid_to : loc -> + val inh_conv_coerce_rigid_to : bool -> loc -> env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] diff -Nru coq-doc-8.4pl2/pretyping/detyping.ml coq-doc-8.4pl4/pretyping/detyping.ml --- coq-doc-8.4pl2/pretyping/detyping.ml 2013-03-18 14:09:52.000000000 +0000 +++ coq-doc-8.4pl4/pretyping/detyping.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* GApp (loc,c,l@[a]) + | GApp (loc,p,l) -> GApp (loc,p,l@[a]) | _ -> (GApp (dl,c,[a]))) in aux n [] c @@ -481,7 +481,7 @@ share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> - if n>0 then warning "Detyping.detype: cannot factorize fix enough"; + if n>0 then msg_warn "Detyping.detype: cannot factorize fix enough"; let c = detype isgoal avoid env c in let t = detype isgoal avoid env t in (List.rev l,c,t) diff -Nru coq-doc-8.4pl2/pretyping/detyping.mli coq-doc-8.4pl4/pretyping/detyping.mli --- coq-doc-8.4pl2/pretyping/detyping.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/pretyping/detyping.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* !debug_unification); + Goptions.optwrite = (fun a -> debug_unification:=a); +} + + type flex_kind_of_term = | Rigid of constr | PseudoRigid of constr (* approximated as rigid but not necessarily so *) @@ -197,7 +208,26 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = + + let eta env evd onleft term l term' l' = + assert (l = []); + let (na,c,body) = destLambda term in + let c = nf_evar evd c in + let env' = push_rel (na,None,c) env in + let appr1 = evar_apprec ts env' evd [] body in + let appr2 = (lift 1 term', List.map (lift 1) l' @ [mkRel 1]) in + if onleft then evar_eqappr_x ts env' evd CONV appr1 appr2 + else evar_eqappr_x ts env' evd CONV appr2 appr1 + in + (* Evar must be undefined since we have flushed evars *) + let () = if !debug_unification then + let open Pp in + let pr_state (tm,l) = + h 0 (Termops.print_constr tm ++ str "|" ++ cut () + ++ prlist_with_sep pr_semicolon + (fun x -> hov 1 (Termops.print_constr x)) l) in + pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) ++ fnl ()) in match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> let f1 i = @@ -382,6 +412,9 @@ solve_simple_eqn (evar_conv_x ts) env evd (position_problem true pbty,ev1,t2) | None -> + if isLambda term2 then + eta env evd false term2 l2 term1 l1 + else (* Postpone the use of an heuristic *) add_conv_pb (pbty,env,applist appr1,applist appr2) evd, true) @@ -396,6 +429,9 @@ solve_simple_eqn (evar_conv_x ts) env evd (position_problem false pbty,ev2,t1) | None -> + if isLambda term1 then + eta env evd true term1 l1 term2 l2 + else (* Postpone the use of an heuristic *) add_conv_pb (pbty,env,applist appr1,applist appr2) evd, true) @@ -408,7 +444,11 @@ match eval_flexible_term ts env flex1 with | Some v1 -> evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2 - | None -> (i,false) + | None -> + if isLambda term2 then + eta env i false term2 l2 term1 l1 + else + (i,false) in ise_try evd [f3; f4] @@ -420,28 +460,20 @@ match eval_flexible_term ts env flex2 with | Some v2 -> evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2) - | None -> (i,false) + | None -> + if isLambda term1 then + eta env i true term1 l1 term2 l2 + else + (i,false) in ise_try evd [f3; f4] (* Eta-expansion *) | Rigid c1, _ when isLambda c1 -> - assert (l1 = []); - let (na,c1,c'1) = destLambda c1 in - let c = nf_evar evd c1 in - let env' = push_rel (na,None,c) env in - let appr1 = evar_apprec ts env' evd [] c'1 in - let appr2 = (lift 1 term2, List.map (lift 1) l2 @ [mkRel 1]) in - evar_eqappr_x ts env' evd CONV appr1 appr2 + eta env evd true term1 l1 term2 l2 | _, Rigid c2 when isLambda c2 -> - assert (l2 = []); - let (na,c2,c'2) = destLambda c2 in - let c = nf_evar evd c2 in - let env' = push_rel (na,None,c) env in - let appr1 = (lift 1 term1, List.map (lift 1) l1 @ [mkRel 1]) in - let appr2 = evar_apprec ts env' evd [] c'2 in - evar_eqappr_x ts env' evd CONV appr1 appr2 + eta env evd false term2 l2 term1 l1 | Rigid c1, Rigid c2 -> begin match kind_of_term c1, kind_of_term c2 with @@ -582,15 +614,21 @@ if subst' = [] then evd, false else Evd.define evk (mkVar (fst (List.hd subst'))) evd, true -let apply_on_subterm f c t = +let apply_on_subterm evdref f c t = let rec applyrec (k,c as kc) t = (* By using eq_constr, we make an approximation, for instance, we *) (* could also be interested in finding a term u convertible to t *) (* such that c occurs in u *) if eq_constr c t then f k else - map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c)) - applyrec kc t + match kind_of_term t with + | Evar (evk,args) when Evd.is_undefined !evdref evk -> + let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in + let g (_,b,_) a = if b = None then applyrec kc a else a in + mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args))) + | _ -> + map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c)) + applyrec kc t in applyrec (0,c) t @@ -598,7 +636,8 @@ let fv1 = free_rels c in let fv2 = collect_vars c in let tyvars = collect_vars ty in - List.map2 (fun (id,_,_) a -> + List.map2 (fun (id,b,_) a -> + b <> None || a == c || (* Here we make an approximation, for instance, we could also be *) (* interested in finding a term u convertible to c such that a occurs *) @@ -670,7 +709,7 @@ evdref := evd; evsref := (fst (destEvar ev),evty)::!evsref; ev in - set_holes evdref (apply_on_subterm set_var c rhs) subst + set_holes evdref (apply_on_subterm evdref set_var c rhs) subst | [] -> rhs in let subst = make_subst (ctxt,args,argoccs) in diff -Nru coq-doc-8.4pl2/pretyping/evarconv.mli coq-doc-8.4pl4/pretyping/evarconv.mli --- coq-doc-8.4pl2/pretyping/evarconv.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/pretyping/evarconv.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* candidates + | Some filter -> + let ids = List.map pi1 (list_filter_with filter (evar_context evi)) in + List.filter (fun a -> list_subset (Idset.elements (collect_vars a)) ids) + candidates + +let filter_candidates evd evk filter candidates_update = let evi = Evd.find_undefined evd evk in - let candidates = match candidates with + let candidates = match candidates_update with | None -> evi.evar_candidates - | Some _ -> candidates in - match candidates,filter with - | None,_ | _, None -> candidates - | Some l, Some filter -> - let ids = List.map pi1 (list_filter_with filter (evar_context evi)) in - Some (List.filter (fun a -> - list_subset (Idset.elements (collect_vars a)) ids) l) + | Some _ -> candidates_update + in + match candidates with + | None -> None + | Some l -> + let l' = filter_effective_candidates evi filter l in + if List.length l = List.length l' && candidates_update = None then + None + else + Some l' let closure_of_filter evd evk filter = let evi = Evd.find_undefined evd evk in @@ -1530,6 +1541,7 @@ exception NotInvertibleUsingOurAlgorithm of constr exception NotEnoughInformationToProgress of (identifier * evar_projection) list +exception NotEnoughInformationEvarEvar of constr exception OccurCheckIn of evar_map * constr let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = @@ -1608,7 +1620,8 @@ with | EvarSolvedOnTheFly (evd,t) -> evdref:=evd; imitate envk t | CannotProject filter' -> - assert !progress; + if not !progress then + raise (NotEnoughInformationEvarEvar t); (* Make the virtual left evar real *) let ty = get_type_of env' !evdref t in let (evd,evar'',ev'') = @@ -1714,6 +1727,8 @@ with | NotEnoughInformationToProgress sols -> postpone_non_unique_projection env evd ev sols rhs + | NotEnoughInformationEvarEvar t -> + add_conv_pb (Reduction.CONV,env,mkEvar ev,t) evd | NotInvertibleUsingOurAlgorithm t -> error_not_clean env evd evk t (evar_source evk evd) | OccurCheckIn (evd,rhs) -> diff -Nru coq-doc-8.4pl2/pretyping/evarutil.mli coq-doc-8.4pl4/pretyping/evarutil.mli --- coq-doc-8.4pl2/pretyping/evarutil.mli 2013-03-30 18:46:05.000000000 +0000 +++ coq-doc-8.4pl4/pretyping/evarutil.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Anonymous -> - (* Unable to manage the presence of both an alias and a variable *) - raise Not_found - | GVar (loc,id) -> PatVar (loc,Name id) - | GHole (loc,_) -> PatVar (loc,na) - | GRef (loc,ConstructRef cstr) -> - PatCstr (loc,cstr,[],na) - | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) -> - let mib,_ = Global.lookup_inductive ind in - let nparams = mib.Declarations.mind_nparams in - if nparams > List.length args then - user_err_loc (loc,"",Pp.str "Invalid notation for pattern."); - let params,args = list_chop nparams args in - List.iter (function GHole _ -> () - | _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern.")) - params; - let args = List.map (cases_pattern_of_glob_constr Anonymous) args in - PatCstr (loc,cstr,args,na) - | _ -> raise Not_found - -let rec cases_pattern_of_glob_constr na = function - | GVar (loc,id) when na<>Anonymous -> (* Unable to manage the presence of both an alias and a variable *) raise Not_found | GVar (loc,id) -> PatVar (loc,Name id) diff -Nru coq-doc-8.4pl2/pretyping/glob_term.mli coq-doc-8.4pl4/pretyping/glob_term.mli --- coq-doc-8.4pl2/pretyping/glob_term.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/pretyping/glob_term.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* sorec stk subst (PApp(h,Array.append a1 a2)) t - | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app -> + | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app -> let p = Array.length args2 - Array.length args1 in if p>=0 then let args21, args22 = array_chop p args2 in let c = mkApp(c2,args21) in - let subst = merge_binding allow_bound_rels stk n c subst in + let subst = + match meta with + | None -> subst + | Some n -> merge_binding allow_bound_rels stk n c subst in array_fold_left2 (sorec stk) subst args1 args22 else raise PatternMatchingFailure diff -Nru coq-doc-8.4pl2/pretyping/matching.mli coq-doc-8.4pl4/pretyping/matching.mli --- coq-doc-8.4pl2/pretyping/matching.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/pretyping/matching.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* env -> evar_map ref -> + bool -> type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment val pretype_type : - val_constraint -> env -> evar_map ref -> + bool -> val_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_type_judgment val pretype_gen : @@ -259,9 +259,9 @@ done (* coerce to tycon if any *) - let inh_conv_coerce_to_tycon loc env evdref j = function + let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function | None -> j - | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t + | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t let push_rels vars env = List.fold_right push_rel vars env @@ -297,18 +297,19 @@ let c = substl subst c in { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> - (* Check if [id] is a section or goal variable *) - try - let (_,_,typ) = lookup_named id env in - { uj_val = mkVar id; uj_type = typ } - with Not_found -> - (* [id] not found, build nice error message if [id] yet known from ltac *) + (* if [id] an ltac variable not bound to a term *) + (* build a nice error message *) try match List.assoc id unbndltacvars with | None -> user_err_loc (loc,"", str "Variable " ++ pr_id id ++ str " should be bound to a term.") | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0 with Not_found -> + (* Check if [id] is a section or goal variable *) + try + let (_,_,typ) = lookup_named id env in + { uj_val = mkVar id; uj_type = typ } + with Not_found -> (* [id] not found, standard error message *) error_var_not_found_loc loc id @@ -346,7 +347,11 @@ (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) - let rec pretype (tycon : type_constraint) env evdref lvar = function + let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = + let pretype = pretype resolve_tc in + let pretype_type = pretype_type resolve_tc in + let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in + match t with | GRef (loc,ref) -> inh_conv_coerce_to_tycon loc env evdref (pretype_ref loc evdref env ref) @@ -459,7 +464,7 @@ | [] -> resj | c::rest -> let argloc = loc_of_glob_constr c in - let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in + let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in let resty = whd_betadeltaiota env !evdref resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> @@ -696,7 +701,7 @@ in inh_conv_coerce_to_tycon loc env evdref cj tycon (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) - and pretype_type valcon env evdref lvar = function + and pretype_type resolve_tc valcon env evdref lvar = function | GHole loc -> (match valcon with | Some v -> @@ -716,7 +721,7 @@ { utj_val = e_new_evar evdref env ~src:loc (mkSort s); utj_type = s}) | c -> - let j = pretype empty_tycon env evdref lvar c in + let j = pretype resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in match valcon with @@ -731,9 +736,9 @@ let c' = match kind with | OfType exptyp -> let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in - (pretype tycon env evdref lvar c).uj_val + (pretype resolve_classes tycon env evdref lvar c).uj_val | IsType -> - (pretype_type empty_valcon env evdref lvar c).utj_val + (pretype_type resolve_classes empty_valcon env evdref lvar c).utj_val in resolve_evars env evdref fail_evar resolve_classes; let c = if expand_evar then nf_evar !evdref c' else c' in @@ -747,14 +752,14 @@ let understand_judgment sigma env c = let evdref = ref sigma in - let j = pretype empty_tycon env evdref ([],[]) c in + let j = pretype true empty_tycon env evdref ([],[]) c in resolve_evars env evdref true true; let j = j_nf_evar !evdref j in check_evars env sigma !evdref (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j let understand_judgment_tcc evdref env c = - let j = pretype empty_tycon env evdref ([],[]) c in + let j = pretype true empty_tycon env evdref ([],[]) c in resolve_evars env evdref false true; j_nf_evar !evdref j diff -Nru coq-doc-8.4pl2/pretyping/pretyping.mli coq-doc-8.4pl4/pretyping/pretyping.mli --- coq-doc-8.4pl2/pretyping/pretyping.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/pretyping/pretyping.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* env -> evar_map ref -> + bool -> type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment val pretype_type : - val_constraint -> env -> evar_map ref -> + bool -> val_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_type_judgment val pretype_gen : diff -Nru coq-doc-8.4pl2/pretyping/recordops.ml coq-doc-8.4pl4/pretyping/recordops.ml --- coq-doc-8.4pl2/pretyping/recordops.ml 2013-03-18 14:09:52.000000000 +0000 +++ coq-doc-8.4pl4/pretyping/recordops.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* + if is_fconv Reduction.CONV env sigma t t1 then Some t2 + else if is_fconv Reduction.CONV env sigma t t2 then Some t1 + else None) + (snd (Evd.extract_all_conv_pbs sigma)) + with + | t::l -> t + | _ -> raise Not_found + else raise Not_found + let rec subst_type env sigma typ = function | [] -> typ | h::rest -> @@ -58,7 +71,12 @@ | Construct cstr -> type_of_constructor env cstr | Case (_,p,c,lf) -> let Inductiveops.IndType(_,realargs) = - try Inductiveops.find_rectype env sigma (type_of env c) + let t = type_of env c in + try Inductiveops.find_rectype env sigma t + with Not_found -> + try + let t = get_type_from_constraints env sigma t in + Inductiveops.find_rectype env sigma t with Not_found -> anomaly "type_of: Bad recursive type" in let t = whd_beta sigma (applist (p, realargs)) in (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with diff -Nru coq-doc-8.4pl2/pretyping/retyping.mli coq-doc-8.4pl4/pretyping/retyping.mli --- coq-doc-8.4pl2/pretyping/retyping.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/pretyping/retyping.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* if wt && flags.check_applied_meta_types then - (let tyM = Typing.meta_type sigma k in - let tyN = get_type_of curenv sigma cN in - check_compatibility curenv substn tyM tyN); + (try + let tyM = Typing.meta_type sigma k in + let tyN = get_type_of curenv sigma cN in + check_compatibility curenv substn tyM tyN + with Anomaly _ (* Hack *) -> + (* Renounce, maybe metas/evars prevents typing *) ()); (* Here we check that [cN] does not contain any local variables *) if nb = 0 then sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst @@ -400,9 +403,12 @@ | _, Meta k when not (dependent cN cM) (* helps early trying alternatives *) -> if wt && flags.check_applied_meta_types then - (let tyM = get_type_of curenv sigma cM in - let tyN = Typing.meta_type sigma k in - check_compatibility curenv substn tyM tyN); + (try + let tyM = get_type_of curenv sigma cM in + let tyN = Typing.meta_type sigma k in + check_compatibility curenv substn tyM tyN + with Anomaly _ (* Hack *) -> + (* Renounce, maybe metas/evars prevents typing *) ()); (* Here we check that [cM] does not contain any local variables *) if nb = 0 then (sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst) @@ -788,7 +794,7 @@ let try_to_coerce env evd c cty tycon = let j = make_judge c cty in - let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in + let (evd',j') = inh_conv_coerce_rigid_to true dummy_loc env evd j tycon in let evd' = Evarconv.consider_remaining_unif_problems env evd' in let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in (evd',j'.uj_val) diff -Nru coq-doc-8.4pl2/pretyping/unification.mli coq-doc-8.4pl4/pretyping/unification.mli --- coq-doc-8.4pl2/pretyping/unification.mli 2012-12-18 00:09:14.000000000 +0000 +++ coq-doc-8.4pl4/pretyping/unification.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] | file :: fl -> - let dirname = Filename.dirname file in - let basename = Filename.basename file in - let modulename = - if Filename.check_suffix basename ".v" then - Filename.chop_suffix basename ".v" + let name_no_suffix = + if Filename.check_suffix file ".v" then + Filename.chop_suffix file ".v" else - basename + file in + let modulename = Filename.basename name_no_suffix in check_module_name modulename; - let file = Filename.concat dirname modulename in (if !verbose then "-compile-verbose" else "-compile") - :: file :: (make_compilation_args fl) + :: name_no_suffix :: (make_compilation_args fl) (* compilation of files [files] with command [command] and args [args] *) @@ -120,7 +118,7 @@ parse (cfiles,args) rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () - | ("-outputstate"|"-inputstate"|"-is" + | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir" |"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib" as o) :: rem -> diff -Nru coq-doc-8.4pl2/scripts/coqmktop.ml coq-doc-8.4pl4/scripts/coqmktop.ml --- coq-doc-8.4pl2/scripts/coqmktop.ml 2013-03-18 14:09:52.000000000 +0000 +++ coq-doc-8.4pl4/scripts/coqmktop.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (str"unfold " ++ pr_evaluable_reference c) | Extern tac -> - (str "(*external*) " ++ Pptactic.pr_glob_tactic (Global.env()) tac) + let env = + try + let (_, env) = Pfedit.get_current_goal_context () in + env + with e when Errors.noncritical e -> Global.env () + in + (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac) let pr_hint (id, v) = (pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ()) diff -Nru coq-doc-8.4pl2/tactics/auto.mli coq-doc-8.4pl4/tactics/auto.mli --- coq-doc-8.4pl2/tactics/auto.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/tactics/auto.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* let sign = pf_filtered_hyps g in match freeze () with - | Some (sign', hints) when Environ.eq_named_context_val sign sign' -> hints + | Some (onlyc, sign', hints) + when onlyc = only_classes && + Environ.eq_named_context_val sign sign' -> hints | _ -> let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in - unfreeze (Some (sign, hints)); hints + unfreeze (Some (only_classes, sign, hints)); hints let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac = { skft = fun sk fk {it = gl,hints; sigma=s} -> diff -Nru coq-doc-8.4pl2/tactics/contradiction.ml coq-doc-8.4pl4/tactics/contradiction.ml --- coq-doc-8.4pl2/tactics/contradiction.ml 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/tactics/contradiction.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* None) let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation +(* Do we have a JMeq instance on twice the same domains ? *) + +let jmeq_same_dom gl = function + | None -> true (* already checked in Hipattern.find_eq_data_decompose *) + | Some t -> + let rels, t = decompose_prod_assum t in + let env = Environ.push_rel_context rels (pf_env gl) in + match decompose_app t with + | _, [dom1; _; dom2;_] -> is_conv env (project gl) dom1 dom2 + | _ -> false + (* find_elim determines which elimination principle is necessary to eliminate lbeq on sort_of_gl. *) -let find_elim hdcncl lft2rgt dep cls args gl = - let inccl = (cls = None) in - if (eq_constr hdcncl (constr_of_reference (Coqlib.glob_eq)) || - eq_constr hdcncl (constr_of_reference (Coqlib.glob_jmeq)) && - pf_conv_x gl (List.nth args 0) (List.nth args 2)) && not dep - || Flags.version_less_or_equal Flags.V8_2 +let find_elim hdcncl lft2rgt dep cls ot gl = + let inccl = not (Option.has_some cls) in + let hdcncl_is u = eq_constr hdcncl (constr_of_reference u) in + if (hdcncl_is (Coqlib.glob_eq) || + hdcncl_is (Coqlib.glob_jmeq) && jmeq_same_dom gl ot) + && not dep + || Flags.version_less_or_equal Flags.V8_2 then match kind_of_term hdcncl with | Ind ind_sp -> @@ -295,7 +307,7 @@ let isatomic = isProd (whd_zeta hdcncl) in let dep_fun = if isatomic then dependent else dependent_no_evar in let dep = dep_proof_ok && dep_fun c (type_of_clause gl cls) in - let elim = find_elim hdcncl lft2rgt dep cls (snd (decompose_app t)) gl in + let elim = find_elim hdcncl lft2rgt dep cls (Some t) gl in general_elim_clause with_evars frzevars tac cls sigma c t l (match lft2rgt with None -> false | Some b -> b) {elimindex = None; elimbody = (elim,NoBindings)} gl @@ -1208,7 +1220,7 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls = (* find substitution scheme *) - let eq_elim = find_elim lbeq.eq (Some false) false None [e1;e2] gls in + let eq_elim = find_elim lbeq.eq (Some false) false None None gls in (* build substitution predicate *) let p = lambda_create (pf_env gls) (t,body) in (* apply substitution scheme *) diff -Nru coq-doc-8.4pl2/tactics/equality.mli coq-doc-8.4pl4/tactics/equality.mli --- coq-doc-8.4pl2/tactics/equality.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/tactics/equality.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [ admit_as_an_axiom ] END -let replace_in_clause_maybe_by (sigma1,c1) c2 in_hyp tac = + + +let classes_dirpath = + make_dirpath (List.map id_of_string ["Classes";"Coq"]) + +let init_setoid () = + if Libnames.is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () + else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"] + + +let occurrences_of occs = + let loccs = match occs with + | n::_ as nl when n < 0 -> (false,List.map (fun n -> ArgArg (abs n)) nl) + | nl -> + if List.exists (fun n -> n < 0) nl then + error "Illegal negative occurrence number."; + (true, List.map (fun n -> (ArgArg n)) nl) + in + init_setoid (); + {onhyps = Some []; concl_occs =loccs} + +let replace_in_clause_maybe_by (sigma1,c1) c2 cl tac = Refiner.tclWITHHOLES false - (replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp)) + (replace_in_clause_maybe_by c1 c2 cl) sigma1 (Option.map Tacinterp.eval_tactic tac) @@ -44,9 +65,15 @@ TACTIC EXTEND replace ["replace" open_constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ] --> [ replace_in_clause_maybe_by c1 c2 in_hyp tac ] +-> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) tac ] END +TACTIC EXTEND replace_at + ["replace" open_constr(c1) "with" constr(c2) "at" occurrences(occs) by_arg_tac(tac) ] +-> [ replace_in_clause_maybe_by c1 c2 (occurrences_of occs) tac ] +END + + TACTIC EXTEND replace_term_left [ "replace" "->" open_constr(c) in_arg_hyp(in_hyp) ] -> [ replace_multi_term (Some true) c in_hyp] diff -Nru coq-doc-8.4pl2/tactics/extratactics.mli coq-doc-8.4pl4/tactics/extratactics.mli --- coq-doc-8.4pl2/tactics/extratactics.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/tactics/extratactics.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* let msg = "No interpretation function found for entry " ^ id in - warning msg; + msg_warn msg; let f = (fun _ _ -> failwith msg), (fun _ _ _ -> failwith msg), (fun _ a -> a) in add_interp_genarg id f; f @@ -967,9 +967,9 @@ (intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x)) | RedExprArgType -> in_gen globwit_red_expr (intern_red_expr ist (out_gen rawwit_red_expr x)) - | OpenConstrArgType b -> - in_gen (globwit_open_constr_gen b) - ((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen b) x))) + | OpenConstrArgType (b1,b2) -> + in_gen (globwit_open_constr_gen (b1,b2)) + ((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen (b1,b2)) x))) | ConstrWithBindingsArgType -> in_gen globwit_constr_with_bindings (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x)) @@ -1290,8 +1290,11 @@ let interp_open_constr_gen kind ist = interp_gen kind ist false true false false -let interp_open_constr ccl ist = - interp_gen (OfType ccl) ist false true false (ccl<>None) +(* wTC is for retrocompatibility: TC resolution started only if needed *) +let interp_open_constr ccl wTC ist e s t = + try interp_gen (OfType ccl) ist false true false (ccl<>None) e s t + with ex when Pretype_errors.precatchable_exception ex && ccl = None && wTC -> + interp_gen (OfType ccl) ist false true false true e s t let interp_pure_open_constr ist = interp_gen (OfType None) ist false false false false @@ -1333,7 +1336,7 @@ let interp_open_constr_list = interp_constr_in_compound_list (fun x -> x) (fun x -> x) - (interp_open_constr None) + (interp_open_constr None false) let interp_auto_lemmas ist env sigma lems = let local_sigma, lems = interp_open_constr_list ist env sigma lems in @@ -1526,7 +1529,7 @@ with Not_found -> NamedHyp id let interp_binding ist env sigma (loc,b,c) = - let sigma, c = interp_open_constr None ist env sigma c in + let sigma, c = interp_open_constr None false ist env sigma c in sigma, (loc,interp_binding_name ist b,c) let interp_bindings ist env sigma = function @@ -1541,12 +1544,12 @@ let interp_constr_with_bindings ist env sigma (c,bl) = let sigma, bl = interp_bindings ist env sigma bl in - let sigma, c = interp_open_constr None ist env sigma c in + let sigma, c = interp_open_constr None false ist env sigma c in sigma, (c,bl) -let interp_open_constr_with_bindings ist env sigma (c,bl) = +let interp_open_constr_with_bindings wTC ist env sigma (c,bl) = let sigma, bl = interp_bindings ist env sigma bl in - let sigma, c = interp_open_constr None ist env sigma c in + let sigma, c = interp_open_constr None wTC ist env sigma c in sigma, (c, bl) let loc_of_bindings = function @@ -1554,11 +1557,11 @@ | ImplicitBindings l -> loc_of_glob_constr (fst (list_last l)) | ExplicitBindings l -> pi1 (list_last l) -let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) = +let interp_open_constr_with_bindings_loc wTC ist env sigma ((c,_),bl as cb) = let loc1 = loc_of_glob_constr c in let loc2 = loc_of_bindings bl in let loc = if loc2 = dummy_loc then loc1 else join_loc loc1 loc2 in - let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in + let sigma, cb = interp_open_constr_with_bindings wTC ist env sigma cb in sigma, (loc,cb) let interp_induction_arg ist gl arg = @@ -1754,8 +1757,8 @@ let mk_constr_value ist gl c = let (sigma,c_interp) = pf_interp_constr ist gl c in sigma,VConstr ([],c_interp) -let mk_open_constr_value ist gl c = - let (sigma,c_interp) = pf_apply (interp_open_constr None ist) gl c in +let mk_open_constr_value wTC ist gl c = + let (sigma,c_interp) = pf_apply (interp_open_constr None wTC ist) gl c in sigma,VConstr ([],c_interp) let mk_hyp_value ist gl c = VConstr ([],mkVar (interp_hyp ist gl c)) let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c) @@ -2132,11 +2135,11 @@ let (sigma,r_interp) = pf_interp_red_expr ist gl (out_gen globwit_red_expr x) in evdref := sigma; in_gen wit_red_expr r_interp - | OpenConstrArgType casted -> - in_gen (wit_open_constr_gen casted) - (interp_open_constr (if casted then Some (pf_concl gl) else None) + | OpenConstrArgType (casted,wTC) -> + in_gen (wit_open_constr_gen (casted,wTC)) + (interp_open_constr (if casted then Some (pf_concl gl) else None) wTC ist (pf_env gl) (project gl) - (snd (out_gen (globwit_open_constr_gen casted) x))) + (snd (out_gen (globwit_open_constr_gen (casted,wTC)) x))) | ConstrWithBindingsArgType -> in_gen wit_constr_with_bindings (pack_sigma (interp_constr_with_bindings ist (pf_env gl) (project gl) @@ -2332,7 +2335,7 @@ (h_vm_cast_no_check c_interp) | TacApply (a,ev,cb,cl) -> let sigma, l = - list_fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb + list_fold_map (interp_open_constr_with_bindings_loc true ist env) sigma cb in let tac = match cl with | None -> h_apply a ev @@ -2547,7 +2550,7 @@ (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> let l = List.map (fun (b,m,c) -> - let f env sigma = interp_open_constr_with_bindings ist env sigma c in + let f env sigma = interp_open_constr_with_bindings false ist env sigma c in (b,m,f)) l in let cl = interp_clause ist gl cl in Equality.general_multi_multi_rewrite ev l cl @@ -2610,8 +2613,12 @@ let (sigma,v) = mk_constr_value ist gl (out_gen globwit_constr x) in evdref := sigma; v - | OpenConstrArgType false -> - let (sigma,v) = mk_open_constr_value ist gl (snd (out_gen globwit_open_constr x)) in + | OpenConstrArgType (false,true) -> + let (sigma,v) = mk_open_constr_value true ist gl (snd (out_gen globwit_open_constr_wTC x)) in + evdref := sigma; + v + | OpenConstrArgType (false,false) -> + let (sigma,v) = mk_open_constr_value false ist gl (snd (out_gen globwit_open_constr x)) in evdref := sigma; v | ConstrMayEvalArgType -> @@ -3013,9 +3020,9 @@ (out_gen globwit_quant_hyp x)) | RedExprArgType -> in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x)) - | OpenConstrArgType b -> - in_gen (globwit_open_constr_gen b) - ((),subst_glob_constr subst (snd (out_gen (globwit_open_constr_gen b) x))) + | OpenConstrArgType (b1,b2) -> + in_gen (globwit_open_constr_gen (b1,b2)) + ((),subst_glob_constr subst (snd (out_gen (globwit_open_constr_gen (b1,b2)) x))) | ConstrWithBindingsArgType -> in_gen globwit_constr_with_bindings (subst_glob_with_bindings subst (out_gen globwit_constr_with_bindings x)) diff -Nru coq-doc-8.4pl2/tactics/tacinterp.mli coq-doc-8.4pl4/tactics/tacinterp.mli --- coq-doc-8.4pl2/tactics/tacinterp.mli 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/tactics/tacinterp.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Environ.env -> Evd.evar_map -> glob_constr_and_expr Glob_term.bindings -> Evd.evar_map * constr Glob_term.bindings -val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map -> +(* first arguments mean wTC (with type classes resolution) *) +val interp_open_constr_with_bindings : bool -> interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr Glob_term.with_bindings -> Evd.evar_map * constr Glob_term.with_bindings (** Initial call for interpretation *) diff -Nru coq-doc-8.4pl2/tactics/tacticals.ml coq-doc-8.4pl4/tactics/tacticals.ml --- coq-doc-8.4pl2/tactics/tacticals.ml 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/tactics/tacticals.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* : use_str : use_str, use_unix : use_str - : use_str, use_unix, thread, ide + : use_str, use_unix, thread, ide, use_camlpX : use_str, use_unix, use_dynlink, use_camlpX : use_nums, use_unix : use_unix - : use_unix + : use_unix, use_camlpX ## tags for ide diff -Nru coq-doc-8.4pl2/test-suite/bench/lists_100.v coq-doc-8.4pl4/test-suite/bench/lists_100.v --- coq-doc-8.4pl2/test-suite/bench/lists_100.v 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/test-suite/bench/lists_100.v 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* V -> Type) (s : V) : V -> Type := + | NoEdges : path E s s + | AddEdge : forall d d' : V, path E s d -> E d d' -> path E s d'. +Inductive G_Vertex := G_v0 | G_v1. +Inductive G_Edge : G_Vertex -> G_Vertex -> Set := G_e : G_Edge G_v0 G_v1. +Goal forall x1 : G_Edge G_v1 G_v1, @AddEdge _ G_Edge G_v1 _ _ (NoEdges _ _) x1 = NoEdges _ _. +intro x1. +try destruct x1. (* now raises a typing error *) diff -Nru coq-doc-8.4pl2/test-suite/bugs/closed/3023.v coq-doc-8.4pl4/test-suite/bugs/closed/3023.v --- coq-doc-8.4pl2/test-suite/bugs/closed/3023.v 1970-01-01 00:00:00.000000000 +0000 +++ coq-doc-8.4pl4/test-suite/bugs/closed/3023.v 2014-04-24 15:13:03.000000000 +0000 @@ -0,0 +1,31 @@ +(* Checking use of eta on Flexible/Rigid and SemiFlexible/Rigid unif problems *) + +Set Implicit Arguments. +Generalizable All Variables. + +Record Category {obj : Type} := + { + Morphism : obj -> obj -> Type; + + Identity : forall x, Morphism x x; + Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'; + LeftIdentity : forall a b (f : Morphism a b), Compose (Identity b) f = f + }. + + +Section DiscreteAdjoints. + Let C := {| + Morphism := (fun X Y : Type => X -> Y); + Identity := (fun X : Type => (fun x : X => x)); + Compose := (fun _ _ _ f g => (fun x => f (g x))); + LeftIdentity := (fun X Y p => @eq_refl _ p : (fun x : X => p x) = p) + |}. + Variable ObjectFunctor : C = C. + + Goal True. + Proof. + subst C. + revert ObjectFunctor. + intro ObjectFunctor. + simpl in ObjectFunctor. + revert ObjectFunctor. (* Used to failed in 8.4 up to 16 April 2013 *) diff -Nru coq-doc-8.4pl2/test-suite/bugs/closed/shouldsucceed/2230.v coq-doc-8.4pl4/test-suite/bugs/closed/shouldsucceed/2230.v --- coq-doc-8.4pl2/test-suite/bugs/closed/shouldsucceed/2230.v 1970-01-01 00:00:00.000000000 +0000 +++ coq-doc-8.4pl4/test-suite/bugs/closed/shouldsucceed/2230.v 2014-04-24 15:13:03.000000000 +0000 @@ -0,0 +1,6 @@ +Goal forall f, f 1 1 -> True. +intros. +match goal with + | [ H : _ ?a |- _ ] => idtac +end. +Abort. diff -Nru coq-doc-8.4pl2/test-suite/bugs/closed/shouldsucceed/2837.v coq-doc-8.4pl4/test-suite/bugs/closed/shouldsucceed/2837.v --- coq-doc-8.4pl2/test-suite/bugs/closed/shouldsucceed/2837.v 1970-01-01 00:00:00.000000000 +0000 +++ coq-doc-8.4pl4/test-suite/bugs/closed/shouldsucceed/2837.v 2014-04-24 15:13:03.000000000 +0000 @@ -0,0 +1,15 @@ +Require Import JMeq. + +Axiom test : forall n m : nat, JMeq n m. + +Goal forall n m : nat, JMeq n m. + +(* I) with no intros nor variable hints, this should produce a regular error + instead of Uncaught exception Failure("nth"). *) +Fail rewrite test. + +(* II) with intros but indication of variables, still an error *) +Fail (intros; rewrite test). + +(* III) a working variant: *) +intros; rewrite (test n m). \ No newline at end of file diff -Nru coq-doc-8.4pl2/test-suite/failure/clash_cons.v coq-doc-8.4pl4/test-suite/failure/clash_cons.v --- coq-doc-8.4pl2/test-suite/failure/clash_cons.v 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/test-suite/failure/clash_cons.v 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* /dev/null 2>&1) +bogomips := ifneq (,$(wildcard /proc/cpuinfo)) sedbogo := -e "s/bogomips.*: \([0-9]*\).*/\1/p" # i386, ppc sedbogo += -e "s/Cpu0Bogo.*: \([0-9]*\).*/\1/p" # sparc diff -Nru coq-doc-8.4pl2/test-suite/misc/berardi_test.v coq-doc-8.4pl4/test-suite/misc/berardi_test.v --- coq-doc-8.4pl2/test-suite/misc/berardi_test.v 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/test-suite/misc/berardi_test.v 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Error: To rename arguments the "rename" flag must be specified. +Argument A renamed to B. The command has indeed failed with message: => Error: To rename arguments the "rename" flag must be specified. +Argument A renamed to T. @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -106,3 +108,6 @@ => Error: Argument z cannot be declared implicit. The command has indeed failed with message: => Error: Extra argument y. +The command has indeed failed with message: +=> Error: To rename arguments the "rename" flag must be specified. +Argument A renamed to R. diff -Nru coq-doc-8.4pl2/test-suite/output/Arguments_renaming.v coq-doc-8.4pl4/test-suite/output/Arguments_renaming.v --- coq-doc-8.4pl2/test-suite/output/Arguments_renaming.v 2011-12-19 16:18:20.000000000 +0000 +++ coq-doc-8.4pl4/test-suite/output/Arguments_renaming.v 2014-04-24 15:13:03.000000000 +0000 @@ -50,5 +50,5 @@ Fail Arguments eq_refl {F F}, [F] F. Fail Arguments eq {F} x [z]. Fail Arguments eq {F} x z y. - +Fail Arguments eq {R} s t. diff -Nru coq-doc-8.4pl2/test-suite/output/Naming.out coq-doc-8.4pl4/test-suite/output/Naming.out --- coq-doc-8.4pl2/test-suite/output/Naming.out 2009-12-03 23:09:05.000000000 +0000 +++ coq-doc-8.4pl4/test-suite/output/Naming.out 2014-04-24 15:13:03.000000000 +0000 @@ -11,7 +11,7 @@ x1 : nat x4 : nat x0 : nat - H : forall x x3 : nat, x + x1 = x4 + x3 + H : forall x5 x6 : nat, x5 + x1 = x4 + x6 ============================ x + x1 = x4 + x0 1 subgoal @@ -51,9 +51,9 @@ x1 : nat x4 : nat x0 : nat - H : forall x x3 : nat, - x + x1 = x4 + x3 -> - forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) + H : forall x5 x6 : nat, + x5 + x1 = x4 + x6 -> + forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1) H0 : x + x1 = x4 + x0 ============================ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x @@ -64,9 +64,9 @@ x1 : nat x4 : nat x0 : nat - H : forall x x3 : nat, - x + x1 = x4 + x3 -> - forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) + H : forall x5 x6 : nat, + x5 + x1 = x4 + x6 -> + forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1) H0 : x + x1 = x4 + x0 x5 : nat x6 : nat @@ -78,6 +78,6 @@ x3 : nat a : nat - H : a = 0 -> forall a : nat, a = 0 + H : a = 0 -> forall a0 : nat, a0 = 0 ============================ a = 0 diff -Nru coq-doc-8.4pl2/test-suite/success/Case19.v coq-doc-8.4pl4/test-suite/success/Case19.v --- coq-doc-8.4pl2/test-suite/success/Case19.v 2006-06-27 21:29:18.000000000 +0000 +++ coq-doc-8.4pl4/test-suite/success/Case19.v 2014-04-24 15:13:03.000000000 +0000 @@ -6,3 +6,14 @@ Variable x : nat*nat. Check let (_, _) := x in sigT (fun _ : T => nat). + +(* This used to raise an anomaly in V8.4, up to pl2 *) + +Goal {x: nat & x=x}. +Fail exists (fun x => + match + projT2 (projT2 x) as e in (_ = y) + return _ = existT _ (projT1 x) (existT _ y e) + with + | eq_refl => eq_refl + end). diff -Nru coq-doc-8.4pl2/test-suite/success/Check.v coq-doc-8.4pl4/test-suite/success/Check.v --- coq-doc-8.4pl2/test-suite/success/Check.v 2012-08-08 18:54:37.000000000 +0000 +++ coq-doc-8.4pl4/test-suite/success/Check.v 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* treat_file None f; parse ll | [] -> () diff -Nru coq-doc-8.4pl2/tools/coqdep_common.ml coq-doc-8.4pl4/tools/coqdep_common.ml --- coq-doc-8.4pl2/tools/coqdep_common.ml 2012-11-02 15:08:47.000000000 +0000 +++ coq-doc-8.4pl4/tools/coqdep_common.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*