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 *)
-(* '.' && f.[0] <> '_' then
+ (* we avoid all files and subdirs starting by '.' (e.g. .svn),
+ plus CVS and _darcs and any subdirs given via -exclude-dirs *)
+ if f.[0] <> '.' then
let phys_f = if phys_dir = "." then f else phys_dir//f in
match try (stat phys_f).st_kind with _ -> S_BLK with
| S_DIR when recur ->
- if List.mem phys_f !norecdir_list then ()
- else
- add_directory recur add_file phys_f (log_dir@[f])
+ if List.mem f !norec_dirnames then ()
+ else
+ if List.mem phys_f !norec_dirs then ()
+ else
+ add_directory recur add_file phys_f (log_dir@[f])
| S_REG -> add_file phys_dir log_dir f
| _ -> ()
done
diff -Nru coq-doc-8.4pl2/tools/coqdep_common.mli coq-doc-8.4pl4/tools/coqdep_common.mli
--- coq-doc-8.4pl2/tools/coqdep_common.mli 2012-08-08 18:54:37.000000000 +0000
+++ coq-doc-8.4pl4/tools/coqdep_common.mli 2014-04-24 15:13:03.000000000 +0000
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* string -> string
diff -Nru coq-doc-8.4pl2/tools/coqdep_lexer.mli coq-doc-8.4pl4/tools/coqdep_lexer.mli
--- coq-doc-8.4pl2/tools/coqdep_lexer.mli 2012-08-08 18:54:37.000000000 +0000
+++ coq-doc-8.4pl4/tools/coqdep_lexer.mli 2014-04-24 15:13:03.000000000 +0000
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* + ]\n";
- flush stderr;
+ eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-R dir coqdir] +\n";
+ eprintf " extra options:\n";
+ eprintf " -coqlib dir : set the coq standard library directory\n";
+ eprintf " -exclude-dir f : skip subdirectories named f during -R search\n";
exit 1
let rec parse = function
@@ -177,9 +178,11 @@
| "-R" :: r :: "-as" :: [] -> usage ()
| "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll
| "-R" :: ([] | [_]) -> usage ()
- | "-coqlib" :: (r :: ll) -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
+ | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll
+ | "-exclude-dir" :: [] -> usage ()
+ | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
| "-coqlib" :: [] -> usage ()
- | "-suffix" :: (s :: ll) -> suffixe := s ; parse ll
+ | "-suffix" :: s :: ll -> suffixe := s ; parse ll
| "-suffix" :: [] -> usage ()
| "-slash" :: ll -> option_slash := true; parse ll
| ("-h"|"--help"|"-help") :: _ -> usage ()
diff -Nru coq-doc-8.4pl2/tools/coqdoc/alpha.ml coq-doc-8.4pl4/tools/coqdoc/alpha.ml
--- coq-doc-8.4pl2/tools/coqdoc/alpha.ml 2012-08-08 18:54:37.000000000 +0000
+++ coq-doc-8.4pl4/tools/coqdoc/alpha.ml 2014-04-24 15:13:03.000000000 +0000
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* exit 1 | _ -> ()
let commands =
- [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (true,false,s)));
- "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (true,true,s)));
- "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (false,false,s)));
- "INTERP", (fun s -> eval_call (Ide_intf.interp (false,true,s)));
+ [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (0,true,false,s)));
+ "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (0,true,true,s)));
+ "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (0,false,false,s)));
+ "INTERP", (fun s -> eval_call (Ide_intf.interp (0,false,true,s)));
"REWIND", (fun s -> eval_call (Ide_intf.rewind (int_of_string s)));
- "GOALS", (fun _ -> eval_call Ide_intf.goals);
- "HINTS", (fun _ -> eval_call Ide_intf.hints);
- "GETOPTIONS", (fun _ -> eval_call Ide_intf.get_options);
- "STATUS", (fun _ -> eval_call Ide_intf.status);
+ "GOALS", (fun _ -> eval_call (Ide_intf.goals ()));
+ "HINTS", (fun _ -> eval_call (Ide_intf.hints ()));
+ "GETOPTIONS", (fun _ -> eval_call (Ide_intf.get_options ()));
+ "STATUS", (fun _ -> eval_call (Ide_intf.status ()));
"INLOADPATH", (fun s -> eval_call (Ide_intf.inloadpath s));
"MKCASES", (fun s -> eval_call (Ide_intf.mkcases s));
"#", (fun _ -> raise Comment);
diff -Nru coq-doc-8.4pl2/tools/gallina_lexer.mll coq-doc-8.4pl4/tools/gallina_lexer.mll
--- coq-doc-8.4pl2/tools/gallina_lexer.mll 2012-08-08 18:54:37.000000000 +0000
+++ coq-doc-8.4pl4/tools/gallina_lexer.mll 2014-04-24 15:13:03.000000000 +0000
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* Flags.V8_3
| "8.2" -> Flags.V8_2
| ("8.1" | "8.0") as s ->
- warning ("Compatibility with version "^s^" not supported.");
+ msg_warn ("Compatibility with version "^s^" not supported.");
Flags.V8_2
| s -> Util.error ("Unknown compatibility version \""^s^"\".")
diff -Nru coq-doc-8.4pl2/toplevel/coqinit.mli coq-doc-8.4pl4/toplevel/coqinit.mli
--- coq-doc-8.4pl2/toplevel/coqinit.mli 2012-08-08 18:54:37.000000000 +0000
+++ coq-doc-8.4pl4/toplevel/coqinit.mli 2014-04-24 15:13:03.000000000 +0000
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* error_same_names_types id
| SameNamesConstructors id -> error_same_names_constructors id
| SameNamesOverlap idl -> error_same_names_overlap idl
- | NotAnArity id -> error_not_an_arity id
+ | NotAnArity (env, c) -> error_not_an_arity env c
| BadEntry -> error_bad_entry ()
| LargeNonPropInductiveNotInType -> error_large_non_prop_inductive_not_in_type ()
diff -Nru coq-doc-8.4pl2/toplevel/himsg.mli coq-doc-8.4pl4/toplevel/himsg.mli
--- coq-doc-8.4pl2/toplevel/himsg.mli 2012-08-08 18:54:37.000000000 +0000
+++ coq-doc-8.4pl4/toplevel/himsg.mli 2014-04-24 15:13:03.000000000 +0000
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* string;
- rewind : int -> int;
- goals : unit -> goals option;
- evars : unit -> evar list option;
- hints : unit -> (hint list * hint) option;
- status : unit -> status;
- search : search_flags -> string coq_object list;
- get_options : unit -> (option_name * option_state) list;
- set_options : (option_name * option_value) list -> unit;
- inloadpath : string -> bool;
- mkcases : string -> string list list;
- quit : unit -> unit;
- about : unit -> coq_info;
- handle_exn : exn -> location * string;
-}
+ | Interp of interp_sty
+ | Rewind of rewind_sty
+ | Goal of goals_sty
+ | Evars of evars_sty
+ | Hints of hints_sty
+ | Status of status_sty
+ | Search of search_sty
+ | GetOptions of get_options_sty
+ | SetOptions of set_options_sty
+ | InLoadPath of inloadpath_sty
+ | MkCases of mkcases_sty
+ | Quit of quit_sty
+ | About of about_sty
+
+type unknown
(** The actual calls *)
-let interp (r,b,s) : string call = Interp (r,b,s)
-let rewind i : int call = Rewind i
-let goals : goals option call = Goal
-let evars : evar list option call = Evars
-let hints : (hint list * hint) option call = Hints
-let status : status call = Status
-let search flags : string coq_object list call = Search flags
-let get_options : (option_name * option_state) list call = GetOptions
-let set_options l : unit call = SetOptions l
-let inloadpath s : bool call = InLoadPath s
-let mkcases s : string list list call = MkCases s
-let quit : unit call = Quit
+let interp x : interp_rty call = Interp x
+let rewind x : rewind_rty call = Rewind x
+let goals x : goals_rty call = Goal x
+let evars x : evars_rty call = Evars x
+let hints x : hints_rty call = Hints x
+let status x : status_rty call = Status x
+let get_options x : get_options_rty call = GetOptions x
+let set_options x : set_options_rty call = SetOptions x
+let inloadpath x : inloadpath_rty call = InLoadPath x
+let mkcases x : mkcases_rty call = MkCases x
+let search x : search_rty call = Search x
+let quit x : quit_rty call = Quit x
(** * Coq answers to CoqIde *)
-let abstract_eval_call handler c =
+let abstract_eval_call handler (c : 'a call) =
+ let mkGood x : 'a value = Good (Obj.magic x) in
try
- let res = match c with
- | Interp (r,b,s) -> Obj.magic (handler.interp (r,b,s) : string)
- | Rewind i -> Obj.magic (handler.rewind i : int)
- | Goal -> Obj.magic (handler.goals () : goals option)
- | Evars -> Obj.magic (handler.evars () : evar list option)
- | Hints -> Obj.magic (handler.hints () : (hint list * hint) option)
- | Status -> Obj.magic (handler.status () : status)
- | Search flags -> Obj.magic (handler.search flags : string coq_object list)
- | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list)
- | SetOptions opts -> Obj.magic (handler.set_options opts : unit)
- | InLoadPath s -> Obj.magic (handler.inloadpath s : bool)
- | MkCases s -> Obj.magic (handler.mkcases s : string list list)
- | Quit -> Obj.magic (handler.quit () : unit)
- | About -> Obj.magic (handler.about () : coq_info)
- in Good res
+ match c with
+ | Interp x -> mkGood (handler.interp x)
+ | Rewind x -> mkGood (handler.rewind x)
+ | Goal x -> mkGood (handler.goals x)
+ | Evars x -> mkGood (handler.evars x)
+ | Hints x -> mkGood (handler.hints x)
+ | Status x -> mkGood (handler.status x)
+ | Search x -> mkGood (handler.search x)
+ | GetOptions x -> mkGood (handler.get_options x)
+ | SetOptions x -> mkGood (handler.set_options x)
+ | InLoadPath x -> mkGood (handler.inloadpath x)
+ | MkCases x -> mkGood (handler.mkcases x)
+ | Quit x -> mkGood (handler.quit x)
+ | About x -> mkGood (handler.about x)
with any ->
- let (l, str) = handler.handle_exn any in
- Fail (l,str)
+ Fail (handler.handle_exn any)
+
+(* To read and typecheck the answers we give a description of the types,
+ and a way to statically check that the reified version is in sync *)
+module ReifType : sig
+
+ type 'a val_t
+
+ val unit_t : unit val_t
+ val string_t : string val_t
+ val int_t : int val_t
+ val bool_t : bool val_t
+ val goals_t : goals val_t
+ val evar_t : evar val_t
+ val state_t : status val_t
+ val coq_info_t : coq_info val_t
+ val option_state_t : option_state val_t
+ val option_t : 'a val_t -> 'a option val_t
+ val list_t : 'a val_t -> 'a list val_t
+ val coq_object_t : 'a val_t -> 'a coq_object val_t
+ val pair_t : 'a val_t -> 'b val_t -> ('a * 'b) val_t
+ val union_t : 'a val_t -> 'b val_t -> ('a ,'b) Util.union val_t
+
+ type value_type = private
+ | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info
+ | Option of value_type
+ | List of value_type
+ | Coq_object of value_type
+ | Pair of value_type * value_type
+ | Union of value_type * value_type
+
+ val check : 'a val_t -> value_type
+
+end = struct
+
+ type value_type =
+ | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info
+ | Option of value_type
+ | List of value_type
+ | Coq_object of value_type
+ | Pair of value_type * value_type
+ | Union of value_type * value_type
+
+ type 'a val_t = value_type
+ let check x = x
+
+ let unit_t = Unit
+ let string_t = String
+ let int_t = Int
+ let bool_t = Bool
+ let goals_t = Goals
+ let evar_t = Evar
+ let state_t = State
+ let coq_info_t = Coq_info
+ let option_state_t = Option_state
+ let option_t x = Option x
+ let list_t x = List x
+ let coq_object_t x = Coq_object x
+ let pair_t x y = Pair (x, y)
+ let union_t x y = Union (x, y)
+
+end
+
+open ReifType
+
+(* For every (call : 'a call), we build the reification of 'a.
+ * In OCaml 4 we could use GATDs to do that I guess *)
+let expected_answer_type call : value_type =
+ let hint = list_t (pair_t string_t string_t) in
+ let hints = pair_t (list_t hint) hint in
+ let options = pair_t (list_t string_t) option_state_t in
+ let objs = coq_object_t string_t in
+ match call with
+ | Interp _ -> check (string_t : interp_rty val_t)
+ | Rewind _ -> check (int_t : rewind_rty val_t)
+ | Goal _ -> check (option_t goals_t : goals_rty val_t)
+ | Evars _ -> check (option_t (list_t evar_t) : evars_rty val_t)
+ | Hints _ -> check (option_t hints : hints_rty val_t)
+ | Status _ -> check (state_t : status_rty val_t)
+ | Search _ -> check (list_t objs : search_rty val_t)
+ | GetOptions _ -> check (list_t options : get_options_rty val_t)
+ | SetOptions _ -> check (unit_t : set_options_rty val_t)
+ | InLoadPath _ -> check (bool_t : inloadpath_rty val_t)
+ | MkCases _ -> check (list_t (list_t string_t) : mkcases_rty val_t)
+ | Quit _ -> check (unit_t : quit_rty val_t)
+ | About _ -> check (coq_info_t : about_rty val_t)
(** * XML data marshalling *)
@@ -113,10 +180,6 @@
else raise Marshal_error
| _ -> raise Marshal_error
-let pcdata = function
-| PCData s -> s
-| _ -> raise Marshal_error
-
let singleton = function
| [x] -> x
| _ -> raise Marshal_error
@@ -132,56 +195,68 @@
let of_unit () = Element ("unit", [], [])
-let to_unit = function
+let to_unit : xml -> unit = function
| Element ("unit", [], []) -> ()
| _ -> raise Marshal_error
-let of_bool b =
+let of_bool (b : bool) : xml =
if b then constructor "bool" "true" []
else constructor "bool" "false" []
-let to_bool xml = do_match xml "bool"
+let to_bool xml : bool = do_match xml "bool"
(fun s _ -> match s with
| "true" -> true
| "false" -> false
| _ -> raise Marshal_error)
-let of_list f l =
+let of_list (f : 'a -> xml) (l : 'a list) =
Element ("list", [], List.map f l)
-let to_list f = function
+let to_list (f : xml -> 'a) : xml -> 'a list = function
| Element ("list", [], l) ->
List.map f l
| _ -> raise Marshal_error
-let of_option f = function
+let of_option (f : 'a -> xml) : 'a option -> xml = function
| None -> Element ("option", ["val", "none"], [])
| Some x -> Element ("option", ["val", "some"], [f x])
-let to_option f = function
+let to_option (f : xml -> 'a) : xml -> 'a option = function
| Element ("option", ["val", "none"], []) -> None
| Element ("option", ["val", "some"], [x]) -> Some (f x)
| _ -> raise Marshal_error
-let of_string s = Element ("string", [], [PCData s])
+let of_string (s : string) : xml = Element ("string", [], [PCData s])
-let to_string = function
+let to_string : xml -> string = function
| Element ("string", [], l) -> raw_string l
| _ -> raise Marshal_error
-let of_int i = Element ("int", [], [PCData (string_of_int i)])
+let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)])
-let to_int = function
+let to_int : xml -> int = function
| Element ("int", [], [PCData s]) ->
(try int_of_string s with Failure _ -> raise Marshal_error)
| _ -> raise Marshal_error
-let of_pair f g (x, y) = Element ("pair", [], [f x; g y])
+let of_pair (f : 'a -> xml) (g : 'b -> xml) : 'a * 'b -> xml =
+ function (x,y) -> Element ("pair", [], [f x; g y])
-let to_pair f g = function
+let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function
| Element ("pair", [], [x; y]) -> (f x, g y)
| _ -> raise Marshal_error
+let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) Util.union -> xml =
+function
+| Util.Inl x -> Element ("union", ["val","in_l"], [f x])
+| Util.Inr x -> Element ("union", ["val","in_r"], [g x])
+
+let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) Util.union=
+function
+| Element ("union", ["val","in_l"], [x]) -> Util.Inl (f x)
+| Element ("union", ["val","in_r"], [x]) -> Util.Inr (g x)
+| _ -> raise Marshal_error
+
(** More elaborate types *)
let of_option_value = function
@@ -275,7 +350,7 @@
let loc_s = int_of_string (List.assoc "loc_s" attrs) in
let loc_e = int_of_string (List.assoc "loc_e" attrs) in
Some (loc_s, loc_e)
- with e when e <> Sys.Break -> None
+ with Not_found | Failure _ -> None
in
let msg = raw_string l in
Fail (loc, msg)
@@ -283,23 +358,24 @@
| _ -> raise Marshal_error
let of_call = function
-| Interp (raw, vrb, cmd) ->
+| Interp (id,raw, vrb, cmd) ->
let flags = (bool_arg "raw" raw) @ (bool_arg "verbose" vrb) in
- Element ("call", ("val", "interp") :: flags, [PCData cmd])
+ Element ("call", ("val", "interp") :: ("id", string_of_int id) :: flags,
+ [PCData cmd])
| Rewind n ->
Element ("call", ("val", "rewind") :: ["steps", string_of_int n], [])
-| Goal ->
+| Goal () ->
Element ("call", ["val", "goal"], [])
-| Evars ->
+| Evars () ->
Element ("call", ["val", "evars"], [])
-| Hints ->
+| Hints () ->
Element ("call", ["val", "hints"], [])
-| Status ->
+| Status () ->
Element ("call", ["val", "status"], [])
| Search flags ->
let args = List.map (of_pair of_search_constraint of_bool) flags in
Element ("call", ["val", "search"], args)
-| GetOptions ->
+| GetOptions () ->
Element ("call", ["val", "getoptions"], [])
| SetOptions opts ->
let args = List.map (of_pair (of_list of_string) of_option_value) opts in
@@ -308,37 +384,40 @@
Element ("call", ["val", "inloadpath"], [PCData file])
| MkCases ind ->
Element ("call", ["val", "mkcases"], [PCData ind])
-| Quit ->
+| Quit () ->
Element ("call", ["val", "quit"], [])
-| About ->
+| About () ->
Element ("call", ["val", "about"], [])
let to_call = function
| Element ("call", attrs, l) ->
let ans = massoc "val" attrs in
begin match ans with
- | "interp" ->
- let raw = List.mem_assoc "raw" attrs in
- let vrb = List.mem_assoc "verbose" attrs in
- Interp (raw, vrb, raw_string l)
+ | "interp" -> begin
+ try
+ let id = List.assoc "id" attrs in
+ let raw = List.mem_assoc "raw" attrs in
+ let vrb = List.mem_assoc "verbose" attrs in
+ Interp (int_of_string id, raw, vrb, raw_string l)
+ with Not_found -> raise Marshal_error end
| "rewind" ->
let steps = int_of_string (massoc "steps" attrs) in
Rewind steps
- | "goal" -> Goal
- | "evars" -> Evars
- | "status" -> Status
+ | "goal" -> Goal ()
+ | "evars" -> Evars ()
+ | "status" -> Status ()
| "search" ->
let args = List.map (to_pair to_search_constraint to_bool) l in
Search args
- | "getoptions" -> GetOptions
+ | "getoptions" -> GetOptions ()
| "setoptions" ->
let args = List.map (to_pair (to_list to_string) to_option_value) l in
SetOptions args
| "inloadpath" -> InLoadPath (raw_string l)
| "mkcases" -> MkCases (raw_string l)
- | "hints" -> Hints
- | "quit" -> Quit
- | "about" -> About
+ | "hints" -> Hints ()
+ | "quit" -> Quit ()
+ | "about" -> About ()
| _ -> raise Marshal_error
end
| _ -> raise Marshal_error
@@ -419,181 +498,216 @@
}
| _ -> raise Marshal_error
+let of_message_level = function
+| Debug s -> constructor "message_level" "debug" [PCData s]
+| Info -> constructor "message_level" "info" []
+| Notice -> constructor "message_level" "notice" []
+| Warning -> constructor "message_level" "warning" []
+| Error -> constructor "message_level" "error" []
+
+let to_message_level xml = do_match xml "message_level"
+ (fun s args -> match s with
+ | "debug" -> Debug (raw_string args)
+ | "info" -> Info
+ | "notice" -> Notice
+ | "warning" -> Warning
+ | "error" -> Error
+ | _ -> raise Marshal_error)
+
+let of_message msg =
+ let lvl = of_message_level msg.message_level in
+ let content = of_string msg.message_content in
+ Element ("message", [], [lvl; content])
+
+let to_message xml = match xml with
+| Element ("message", [], [lvl; content]) ->
+ { message_level = to_message_level lvl; message_content = to_string content }
+| _ -> raise Marshal_error
+
+let is_message = function
+| Element ("message", _, _) -> true
+| _ -> false
+
+let of_loc loc =
+ let start, stop = loc in
+ Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[])
+
+let to_loc xml = match xml with
+| Element ("loc", l,[]) ->
+ (try
+ let start = List.assoc "start" l in
+ let stop = List.assoc "stop" l in
+ (int_of_string start, int_of_string stop)
+ with Not_found | Invalid_argument _ -> raise Marshal_error)
+| _ -> raise Marshal_error
+
+let to_feedback_content xml = do_match xml "feedback_content"
+ (fun s args -> match s with
+ | "addedaxiom" -> AddedAxiom
+ | "processed" -> Processed
+ | "globref" ->
+ (match args with
+ | [loc; filepath; modpath; ident; ty] ->
+ GlobRef(to_loc loc, to_string filepath, to_string modpath,
+ to_string ident, to_string ty)
+ | _ -> raise Marshal_error)
+ | _ -> raise Marshal_error)
+
+let of_feedback_content = function
+| AddedAxiom -> constructor "feedback_content" "addedaxiom" []
+| Processed -> constructor "feedback_content" "processed" []
+| GlobRef(loc, filepath, modpath, ident, ty) ->
+ constructor "feedback_content" "globref" [
+ of_loc loc;
+ of_string filepath;
+ of_string modpath;
+ of_string ident;
+ of_string ty
+ ]
+
+let of_feedback msg =
+ let content = of_feedback_content msg.content in
+ Element ("feedback", ["id",string_of_int msg.edit_id], [content])
+
+let to_feedback xml = match xml with
+| Element ("feedback", ["id",id], [content]) ->
+ { edit_id = int_of_string id;
+ content = to_feedback_content content }
+| _ -> raise Marshal_error
+
+let is_feedback = function
+| Element ("feedback", _, _) -> true
+| _ -> false
+
(** Conversions between ['a value] and xml answers
When decoding an xml answer, we dynamically check that it is compatible
with the original call. For that we now rely on the fact that all
sub-fonctions [to_xxx : xml -> xxx] check that the current xml element
- is "xxx", and raise [Marshal_error] if anything goes wrong.
-*)
-
-type value_type =
- | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info
- | Option of value_type
- | List of value_type
- | Coq_object of value_type
- | Pair of value_type * value_type
-
-let hint = List (Pair (String, String))
-let option_name = List String
-
-let expected_answer_type = function
- | Interp _ -> String
- | Rewind _ -> Int
- | Goal -> Option Goals
- | Evars -> Option (List Evar)
- | Hints -> Option (Pair (List hint, hint))
- | Status -> State
- | Search _ -> List (Coq_object String)
- | GetOptions -> List (Pair (option_name, Option_state))
- | SetOptions _ -> Unit
- | InLoadPath _ -> Bool
- | MkCases _ -> List (List String)
- | Quit -> Unit
- | About -> Coq_info
+ is "xxx", and raise [Marshal_error] if anything goes wrong. *)
let of_answer (q : 'a call) (r : 'a value) : xml =
let rec convert ty : 'a -> xml = match ty with
- | Unit -> Obj.magic of_unit
- | Bool -> Obj.magic of_bool
- | String -> Obj.magic of_string
- | Int -> Obj.magic of_int
- | State -> Obj.magic of_status
- | Option_state -> Obj.magic of_option_state
- | Coq_info -> Obj.magic of_coq_info
- | Goals -> Obj.magic of_goals
- | Evar -> Obj.magic of_evar
- | List t -> Obj.magic (of_list (convert t))
- | Option t -> Obj.magic (of_option (convert t))
- | Coq_object t -> Obj.magic (of_coq_object (convert t))
- | Pair (t1,t2) -> Obj.magic (of_pair (convert t1) (convert t2))
+ | Unit -> Obj.magic of_unit
+ | Bool -> Obj.magic of_bool
+ | String -> Obj.magic of_string
+ | Int -> Obj.magic of_int
+ | State -> Obj.magic of_status
+ | Option_state -> Obj.magic of_option_state
+ | Coq_info -> Obj.magic of_coq_info
+ | Goals -> Obj.magic of_goals
+ | Evar -> Obj.magic of_evar
+ | List t -> Obj.magic (of_list (convert t))
+ | Option t -> Obj.magic (of_option (convert t))
+ | Coq_object t -> Obj.magic (of_coq_object (convert t))
+ | Pair (t1,t2) -> Obj.magic (of_pair (convert t1) (convert t2))
+ | Union (t1,t2) -> Obj.magic (of_union (convert t1) (convert t2))
in
of_value (convert (expected_answer_type q)) r
let to_answer xml (c : 'a call) : 'a value =
let rec convert ty : xml -> 'a = match ty with
- | Unit -> Obj.magic to_unit
- | Bool -> Obj.magic to_bool
- | String -> Obj.magic to_string
- | Int -> Obj.magic to_int
- | State -> Obj.magic to_status
- | Option_state -> Obj.magic to_option_state
- | Coq_info -> Obj.magic to_coq_info
- | Goals -> Obj.magic to_goals
- | Evar -> Obj.magic to_evar
- | List t -> Obj.magic (to_list (convert t))
- | Option t -> Obj.magic (to_option (convert t))
- | Coq_object t -> Obj.magic (to_coq_object (convert t))
- | Pair (t1,t2) -> Obj.magic (to_pair (convert t1) (convert t2))
+ | Unit -> Obj.magic to_unit
+ | Bool -> Obj.magic to_bool
+ | String -> Obj.magic to_string
+ | Int -> Obj.magic to_int
+ | State -> Obj.magic to_status
+ | Option_state -> Obj.magic to_option_state
+ | Coq_info -> Obj.magic to_coq_info
+ | Goals -> Obj.magic to_goals
+ | Evar -> Obj.magic to_evar
+ | List t -> Obj.magic (to_list (convert t))
+ | Option t -> Obj.magic (to_option (convert t))
+ | Coq_object t -> Obj.magic (to_coq_object (convert t))
+ | Pair (t1,t2) -> Obj.magic (to_pair (convert t1) (convert t2))
+ | Union (t1,t2) -> Obj.magic (to_union (convert t1) (convert t2))
in
to_value (convert (expected_answer_type c)) xml
(** * Debug printing *)
+let pr_unit () = ""
+let pr_string s = Printf.sprintf "%S" s
+let pr_int i = string_of_int i
+let pr_bool b = Printf.sprintf "%B" b
+let pr_goal (g : goals) =
+ if g.fg_goals = [] then
+ if g.bg_goals = [] then "Proof completed."
+ else
+ let rec pr_focus _ = function
+ | [] -> assert false
+ | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg)
+ | (lg, rg) :: l ->
+ Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l in
+ Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
+ else
+ let pr_menu s = s in
+ let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
+ "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^
+ pr_menu goal ^ "]" in
+ String.concat " " (List.map pr_goal g.fg_goals)
+let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]"
+let pr_status (s : status) =
+ let path =
+ let l = String.concat "." s.status_path in
+ "path=" ^ l ^ ";" in
+ let name = match s.status_proofname with
+ | None -> "no proof;"
+ | Some n -> "proof = " ^ n ^ ";" in
+ "Status: " ^ path ^ name
+let pr_coq_info (i : coq_info) = "FIXME"
let pr_option_value = function
-| IntValue None -> "none"
-| IntValue (Some i) -> string_of_int i
-| StringValue s -> s
-| BoolValue b -> if b then "true" else "false"
-
-let rec pr_setoptions opts =
- let map (key, v) =
- let key = String.concat " " key in
- key ^ " := " ^ (pr_option_value v)
- in
- String.concat "; " (List.map map opts)
-
-let pr_getoptions opts =
- let map (key, s) =
- let key = String.concat " " key in
- Printf.sprintf "%s: sync := %b; depr := %b; name := %s; value := %s\n"
- key s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value)
- in
- "\n" ^ String.concat "" (List.map map opts)
+ | IntValue None -> "none"
+ | IntValue (Some i) -> string_of_int i
+ | StringValue s -> s
+ | BoolValue b -> if b then "true" else "false"
+let pr_option_state (s : option_state) =
+ Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n"
+ s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value)
+let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]"
+let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")"
+let pr_coq_object (o : 'a coq_object) = "FIXME"
+let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")"
+let pr_union pr1 pr2 = function Util.Inl x -> pr1 x | Util.Inr x -> pr2 x
let pr_call = function
- | Interp (r,b,s) ->
+ | Interp (id,r,b,s) ->
let raw = if r then "RAW" else "" in
let verb = if b then "" else "SILENT" in
- "INTERP"^raw^verb^" ["^s^"]"
+ "INTERP"^raw^verb^" "^string_of_int id^" ["^s^"]"
| Rewind i -> "REWIND "^(string_of_int i)
- | Goal -> "GOALS"
- | Evars -> "EVARS"
- | Hints -> "HINTS"
- | Status -> "STATUS"
+ | Goal _ -> "GOALS"
+ | Evars _ -> "EVARS"
+ | Hints _ -> "HINTS"
+ | Status _ -> "STATUS"
| Search _ -> "SEARCH"
- | GetOptions -> "GETOPTIONS"
- | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]"
+ | GetOptions _ -> "GETOPTIONS"
+ | SetOptions l -> "SETOPTIONS" ^ " [" ^
+ String.concat ";"
+ (List.map (pr_pair (pr_list pr_string) pr_option_value) l) ^ "]"
| InLoadPath s -> "INLOADPATH "^s
| MkCases s -> "MKCASES "^s
- | Quit -> "QUIT"
- | About -> "ABOUT"
-
+ | Quit _ -> "QUIT"
+ | About _ -> "ABOUT"
let pr_value_gen pr = function
| Good v -> "GOOD " ^ pr v
| Fail (_,str) -> "FAIL ["^str^"]"
-
-let pr_value v = pr_value_gen (fun _ -> "") v
-
-let pr_string s = "["^s^"]"
-let pr_bool b = if b then "true" else "false"
-
-let pr_status s =
- let path =
- let l = String.concat "." s.status_path in
- "path=" ^ l ^ ";"
- in
- let name = match s.status_proofname with
- | None -> "no proof;"
- | Some n -> "proof = " ^ n ^ ";"
- in
- "Status: " ^ path ^ name
-
-let pr_mkcases l =
- let l = List.map (String.concat " ") l in
- "[" ^ String.concat " | " l ^ "]"
-
-let pr_goals_aux g =
- if g.fg_goals = [] then
- if g.bg_goals = [] then "Proof completed."
- else
- let rec pr_focus _ = function
- | [] -> assert false
- | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg)
- | (lg, rg) :: l ->
- Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l
- in
- Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
- else
- let pr_menu s = s in
- let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
- "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ pr_menu goal ^ "]"
- in
- String.concat " " (List.map pr_goal g.fg_goals)
-
-let pr_goals = function
-| None -> "No proof in progress."
-| Some g -> pr_goals_aux g
-
-let pr_evar ev = "[" ^ ev.evar_info ^ "]"
-
-let pr_evars = function
-| None -> "No proof in progress."
-| Some evars -> String.concat " " (List.map pr_evar evars)
-
+let pr_value v = pr_value_gen (fun _ -> "FIXME") v
let pr_full_value call value =
- match call with
- | Interp _ -> pr_value_gen pr_string (Obj.magic value : string value)
- | Rewind i -> pr_value_gen string_of_int (Obj.magic value : int value)
- | Goal -> pr_value_gen pr_goals (Obj.magic value : goals option value)
- | Evars -> pr_value_gen pr_evars (Obj.magic value : evar list option value)
- | Hints -> pr_value value
- | Status -> pr_value_gen pr_status (Obj.magic value : status value)
- | Search _ -> pr_value value
- | GetOptions -> pr_value_gen pr_getoptions (Obj.magic value : (option_name * option_state) list value)
- | SetOptions _ -> pr_value value
- | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value)
- | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value)
- | Quit -> pr_value value
- | About -> pr_value value
-
+ let rec pr = function
+ | Unit -> Obj.magic pr_unit
+ | Bool -> Obj.magic pr_bool
+ | String -> Obj.magic pr_string
+ | Int -> Obj.magic pr_int
+ | State -> Obj.magic pr_status
+ | Option_state -> Obj.magic pr_option_state
+ | Coq_info -> Obj.magic pr_coq_info
+ | Goals -> Obj.magic pr_goal
+ | Evar -> Obj.magic pr_evar
+ | List t -> Obj.magic (pr_list (pr t))
+ | Option t -> Obj.magic (pr_option (pr t))
+ | Coq_object t -> Obj.magic pr_coq_object
+ | Pair (t1,t2) -> Obj.magic (pr_pair (pr t1) (pr t2))
+ | Union (t1,t2) -> Obj.magic (pr_union (pr t1) (pr t2))
+ in
+ pr_value_gen (pr (expected_answer_type call)) value
diff -Nru coq-doc-8.4pl2/toplevel/ide_intf.mli coq-doc-8.4pl4/toplevel/ide_intf.mli
--- coq-doc-8.4pl2/toplevel/ide_intf.mli 2012-11-20 16:40:40.000000000 +0000
+++ coq-doc-8.4pl4/toplevel/ide_intf.mli 2014-04-24 15:13:03.000000000 +0000
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* string call
-
-(** Backtracking by at least a certain number of phrases.
- No finished proofs will be re-opened. Instead,
- we continue backtracking until before these proofs,
- and answer the amount of extra backtracking performed.
- Backtracking by more than the number of phrases already
- interpreted successfully (and not yet undone) will fail. *)
-val rewind : int -> int call
-
-(** Fetching the list of current goals. Return [None] if no proof is in
- progress, [Some gl] otherwise. *)
-val goals : goals option call
-
-(** Retrieving the tactics applicable to the current goal. [None] if there is
- no proof in progress. *)
-val hints : (hint list * hint) option call
-
-(** The status, for instance "Ready in SomeSection, proving Foo" *)
-val status : status call
-
-(** Is a directory part of Coq's loadpath ? *)
-val inloadpath : string -> bool call
-
-(** Create a "match" template for a given inductive type.
- For each branch of the match, we list the constructor name
- followed by enough pattern variables. *)
-val mkcases : string -> string list list call
-
-(** Retrieve the list of unintantiated evars in the current proof. [None] if no
- proof is in progress. *)
-val evars : evar list option call
-
-(** Retrieve the list of options of the current toplevel, together with their
- state. *)
-val get_options : (option_name * option_state) list call
-
-(** Set the options to the given value. Warning: this is not atomic, so whenever
- the call fails, the option state can be messed up... This is the caller duty
- to check that everything is correct. *)
-val set_options : (option_name * option_value) list -> unit call
-
-(** Quit gracefully the interpreter. *)
-val quit : unit call
-
-(** The structure that coqtop should implement *)
-
-type handler = {
- interp : raw * verbose * string -> string;
- rewind : int -> int;
- goals : unit -> goals option;
- evars : unit -> evar list option;
- hints : unit -> (hint list * hint) option;
- status : unit -> status;
- search : search_flags -> string coq_object list;
- get_options : unit -> (option_name * option_state) list;
- set_options : (option_name * option_value) list -> unit;
- inloadpath : string -> bool;
- mkcases : string -> string list list;
- quit : unit -> unit;
- about : unit -> coq_info;
- handle_exn : exn -> location * string;
-}
+type unknown
+
+val interp : interp_sty -> interp_rty call
+val rewind : rewind_sty -> rewind_rty call
+val goals : goals_sty -> goals_rty call
+val hints : hints_sty -> hints_rty call
+val status : status_sty -> status_rty call
+val inloadpath : inloadpath_sty -> inloadpath_rty call
+val mkcases : mkcases_sty -> mkcases_rty call
+val evars : evars_sty -> evars_rty call
+val search : search_sty -> search_rty call
+val get_options : get_options_sty -> get_options_rty call
+val set_options : set_options_sty -> set_options_rty call
+val quit : quit_sty -> quit_rty call
val abstract_eval_call : handler -> 'a call -> 'a value
@@ -97,11 +39,18 @@
exception Marshal_error
+val of_call : 'a call -> xml
+val to_call : xml -> unknown call
+
+val of_message : message -> xml
+val to_message : xml -> message
+val is_message : xml -> bool
+
val of_value : ('a -> xml) -> 'a value -> xml
-val to_value : (xml -> 'a) -> xml -> 'a value
-val of_call : 'a call -> xml
-val to_call : xml -> 'a call
+val of_feedback : feedback -> xml
+val to_feedback : xml -> feedback
+val is_feedback : xml -> bool
val of_answer : 'a call -> 'a value -> xml
val to_answer : xml -> 'a call -> 'a value
diff -Nru coq-doc-8.4pl2/toplevel/ide_slave.ml coq-doc-8.4pl4/toplevel/ide_slave.ml
--- coq-doc-8.4pl2/toplevel/ide_slave.ml 2013-03-18 14:09:52.000000000 +0000
+++ coq-doc-8.4pl4/toplevel/ide_slave.ml 2014-04-24 15:13:03.000000000 +0000
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* raise Quit);
- Ide_intf.about = interruptible about;
- Ide_intf.handle_exn = handle_exn; }
+ Interface.interp = interruptible interp;
+ Interface.rewind = interruptible Backtrack.back;
+ Interface.goals = interruptible goals;
+ Interface.evars = interruptible evars;
+ Interface.hints = interruptible hints;
+ Interface.status = interruptible status;
+ Interface.search = interruptible search;
+ Interface.inloadpath = interruptible inloadpath;
+ Interface.get_options = interruptible get_options;
+ Interface.set_options = interruptible set_options;
+ Interface.mkcases = interruptible Vernacentries.make_cases;
+ Interface.quit = (fun () -> raise Quit);
+ Interface.about = interruptible about;
+ Interface.handle_exn = handle_exn; }
in
(* If the messages of last command are still there, we remove them *)
ignore (read_stdout ());
diff -Nru coq-doc-8.4pl2/toplevel/ide_slave.mli coq-doc-8.4pl4/toplevel/ide_slave.mli
--- coq-doc-8.4pl2/toplevel/ide_slave.mli 2012-08-08 18:54:37.000000000 +0000
+++ coq-doc-8.4pl4/toplevel/ide_slave.mli 2014-04-24 15:13:03.000000000 +0000
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* interp_rty;
+ rewind : rewind_sty -> rewind_rty;
+ goals : goals_sty -> goals_rty;
+ evars : evars_sty -> evars_rty;
+ hints : hints_sty -> hints_rty;
+ status : status_sty -> status_rty;
+ search : search_sty -> search_rty;
+ get_options : get_options_sty -> get_options_rty;
+ set_options : set_options_sty -> set_options_rty;
+ inloadpath : inloadpath_sty -> inloadpath_rty;
+ mkcases : mkcases_sty -> mkcases_rty;
+ quit : quit_sty -> quit_rty;
+ about : about_sty -> about_rty;
+ handle_exn : handle_exn_sty -> handle_exn_rty;
+}
+
diff -Nru coq-doc-8.4pl2/toplevel/lemmas.ml coq-doc-8.4pl4/toplevel/lemmas.ml
--- coq-doc-8.4pl2/toplevel/lemmas.ml 2013-02-20 12:32:01.000000000 +0000
+++ coq-doc-8.4pl4/toplevel/lemmas.ml 2014-04-24 15:13:03.000000000 +0000
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* warning "This notation will not be used for printing as it is bound to a \nsingle variable"; true
+ | AVar _ -> msg_warn "This notation will not be used for printing as it is bound to a \nsingle variable"; true
| _ -> false
let find_precedence lev etyps symbols =
@@ -909,7 +909,7 @@
(match next' with
| Terminal "}" as t2 :: l'' as l1 ->
if l <> l0 or l' <> l1 then
- warning "Skipping spaces inside curly brackets";
+ msg_warn "Skipping spaces inside curly brackets";
if deb & l'' = [] then [t1;x;t2] else begin
check_curly_brackets_notation_exists ();
x :: aux false l''
diff -Nru coq-doc-8.4pl2/toplevel/metasyntax.mli coq-doc-8.4pl4/toplevel/metasyntax.mli
--- coq-doc-8.4pl2/toplevel/metasyntax.mli 2012-08-08 18:54:37.000000000 +0000
+++ coq-doc-8.4pl4/toplevel/metasyntax.mli 2014-04-24 15:13:03.000000000 +0000
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* t.use_file s
- | _ -> warning "Cannot access the ML compiler"
+ | _ -> msg_warn "Cannot access the ML compiler"
(* Adds a path to the ML paths *)
let add_ml_dir s =
diff -Nru coq-doc-8.4pl2/toplevel/mltop.mli coq-doc-8.4pl4/toplevel/mltop.mli
--- coq-doc-8.4pl2/toplevel/mltop.mli 2012-08-08 18:54:37.000000000 +0000
+++ coq-doc-8.4pl4/toplevel/mltop.mli 2014-04-24 15:13:03.000000000 +0000
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(*
begin
try Sys.chdir (System.expand_path_macros path)
- with Sys_error str -> warning ("Cd failed: " ^ str)
+ with Sys_error str -> msg_warn ("Cd failed: " ^ str)
end;
if_verbose message (Sys.getcwd())
@@ -883,6 +883,12 @@
| x, _ -> x in
List.map (fun ns -> List.map name_anons (List.combine ns inf_names)) l in
let names_decl = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
+ let renamed_arg = ref None in
+ let set_renamed a b =
+ if !renamed_arg = None && a <> b then renamed_arg := Some(b,a) in
+ let pr_renamed_arg () = match !renamed_arg with None -> ""
+ | Some (o,n) ->
+ "\nArgument "^string_of_id o ^" renamed to "^string_of_id n^"." in
let some_renaming_specified =
try Arguments_renaming.arguments_names sr <> names_decl
with Not_found -> false in
@@ -894,15 +900,19 @@
| (Name x, _,_, true, _), Anonymous ->
error ("Argument "^string_of_id x^" cannot be declared implicit.")
| (Name iid, _,_, true, max), Name id ->
+ set_renamed iid id;
b || iid <> id, Some (ExplByName id, max, false)
- | (Name iid, _,_, _, _), Name id -> b || iid <> id, None
+ | (Name iid, _,_, _, _), Name id ->
+ set_renamed iid id;
+ b || iid <> id, None
| _ -> b, None)
sr (List.combine il inf_names) in
sr || sr', Util.list_map_filter (fun x -> x) impl)
some_renaming_specified l in
if some_renaming_specified then
if not (List.mem `Rename flags) then
- error "To rename arguments the \"rename\" flag must be specified."
+ error ("To rename arguments the \"rename\" flag must be specified."
+ ^ pr_renamed_arg ())
else Arguments_renaming.rename_arguments local sr names_decl;
(* All other infos are in the first item of l *)
let l = List.hd l in
diff -Nru coq-doc-8.4pl2/toplevel/vernacentries.mli coq-doc-8.4pl4/toplevel/vernacentries.mli
--- coq-doc-8.4pl2/toplevel/vernacentries.mli 2012-08-08 18:54:37.000000000 +0000
+++ coq-doc-8.4pl4/toplevel/vernacentries.mli 2014-04-24 15:13:03.000000000 +0000
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(*