coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu	2014-12-12
\| \| \| \|	Documentation also updated.
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
\|
*	refman: switch all source files to utf8	Pierre Letouzey	2014-12-09
\| \| \| \| \| \|	Putting utf8 everywhere helps the maintainance of the online refman. And anyway, this is the way to go. We should also chase and migrate the few remaining iso-latin-1 files elsewhere in the sources.
*	refman: fix broken urls	Pierre Letouzey	2014-12-09
\|
*	refman: remove ?uri=referer in urls pointing to validator.w3.org	Pierre Letouzey	2014-12-09
\| \| \| \| \| \| \| \| \| \| \|	Unfortunately, these ?uri=referer parameters do not work correctly now that coq.inria.fr forces the switch to https before answering any document. See: http://validator.w3.org/docs/help.html#faq-referer I currently see no workaround for that, apart from generating links like ?uri=http://the.real.url/of/my/page, which would be quite painful. For now, users interested in checking the validity of our pages will have to copy-paste the url they want to check after clicking on the validator button.
*	refman/Omega.tex: do not advertize Pierre Cregut's email for bug reports	Pierre Letouzey	2014-12-09
\|
*	refman/coqdoc.tex: fix two erroneous \url	Pierre Letouzey	2014-12-09
\|
*	refman: for xhtml validity, add 'alt' attributes to img	Pierre Letouzey	2014-12-09
\|
*	refman: avoid label names with whitespace (unsupported in html)	Pierre Letouzey	2014-12-09
\|
*	refman: xhtml validity of the cover page	Pierre Letouzey	2014-12-09
\|
*	doc/stdlib: fix the xhtml validity of the index-list template	Pierre Letouzey	2014-12-09
\|
*	doc: improved xhtml compatibility (cover, header,...)	Pierre Letouzey	2014-12-09
\|
*	doc/stdlib: fix the html charset in header.html and co	Pierre Letouzey	2014-12-09
\|
*	doc: version number in cover.html + updates in coq.inria.fr style	Pierre Letouzey	2014-12-09
\| \| \| \|	To be continued someday, those style files are full of redundancies...
*	Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la ↵	notin	2014-12-09
\| \| \| \|	documentation en ligne)
*	Port to trunk the old commit r14895 of v8.4 (styles for the stdlib ↵	notin	2014-12-09
\| \| \| \| \| \|	documentation) This commit r14895 comes apparently itself from commit r12010 in branch v8.2
*	Documenting the Set Refine Instance Mode.	Pierre-Marie Pédrot	2014-11-30
\|
*	FAQ: fix some broken urls	Pierre Letouzey	2014-11-27
\|
*	typos	Enrico Tassi	2014-11-27
\|
*	Documenting the -color option.	Pierre-Marie Pédrot	2014-11-17
\|
*	Documenting use of colors in Coq.	Pierre-Marie Pédrot	2014-11-17
\|
*	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin	2014-11-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	reference" and "simpl pattern" in the code (maybe we should have merged them instead, but I finally decided to enforce their difference, even if some compatibility is to be preversed - the idea is that at some time "simpl reference" would only call a weak-head simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n) rather than S(S(n)) which could be useful for better using induction hypotheses. In the process we also implement the following: - 'simpl "+"' is accepted to reduce all applicative subterms whose head symbol is written "+" (in the toplevel scope); idem for vm_compute and native_compute - 'simpl reference' works even if reference has maximally inserted implicit arguments (this solves the "simpl fst" incompatibility) - compatibility of ltac expressions referring to vm_compute and native_compute with functor application should now work (i.e. vm_compute and native_compute are now taken into account in tacsubst.ml) - for compatibility, "simpl eq" (assuming no maximal implicit args in eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed. By the way, is "mul" on nat defined optimally? "3*n" simplifies to "n+(n+(n+0))". Are there some advantages of this compared to have it simplified to "n+n+n" (i.e. to "(n+n)+n").
*	Document (some) Proof using syntax + the new Optimize commands	Enrico Tassi	2014-11-12
\|
*	Fixing doc of Functional Induction.	Hugo Herbelin	2014-11-07
\|
*	doc: version number in cover.html + updates in coq.inria.fr style	Pierre Letouzey	2014-11-07
\|
*	Documenting the change of semantics of the replace tactic.	Pierre-Marie Pédrot	2014-11-04
\|
*	Document [Info] command.	Arnaud Spiwack	2014-11-01
\|
*	Use the url package, since coqdoc generates \url commands.	Guillaume Melquiond	2014-10-27
\|
*	Addressing report #3279 (inconsistency of behavior of the -> and <-	Hugo Herbelin	2014-10-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	introduction patterns). Whether we call -> and <- from assert as or apply in as, or as a component of a larger introduction pattern, the new documented semantics is: - behave as subst if an equation rewriting a variable (rewrite in conclusion and hyps and erase variable and hyp). - rewrite in concl if an equation not rewrite a variable or a quantified equality, then erase the hypothesis. This is potential source of incompatibilities.
*	Fix typo in documentation of the [repeat] tactical.	Arnaud Spiwack	2014-10-24
\| \| \|	Closes #3761.
*	Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)	Enrico Tassi	2014-10-22
\|
*	More fallout from elisp rename	Anders Kaseorg	2014-10-16
\| \| \| \| \| \| \| \| \| \|	Commit 3e972b3ff8e532be233f70567c87512324c99b4e renamed coq.el, coq-db.el, coq-syntax.el to gallina.el, gallina-db.el, gallina-syntax.el without fixing up any of the references. Commit 30b58d43e48569afb50a35d3915ec7d453a61f5d only fixed up some of them. Here are some more (hopefully all of them). Signed-off-by: Anders Kaseorg <andersk@mit.edu>
*	Fixing #3606 continued (doc of Scheme Boolean Equality Scheme).	Hugo Herbelin	2014-10-03
\|
*	Removing deactivated command Show Tree.	Hugo Herbelin	2014-10-03
\|
*	typo	Enrico Tassi	2014-09-29
\|
*	Documenting option -type-in-type.	Hugo Herbelin	2014-09-29
\|
*	seems to fix a looping coq-tex (when compiled with camlp4)	Pierre Boutillier	2014-09-18
\|
*	Fixing bug #3605.	Pierre-Marie Pédrot	2014-09-11
\|
*	Removing remaining documentation of the XML plugin.	Pierre-Marie Pédrot	2014-09-11
\|
*	Fixing inversion after having fixed intros_replacing	Hugo Herbelin	2014-09-10
\| \| \| \| \| \| \|	in69665dd2480d364162933972de7ffa955eccab4d. There are still situations when "as" is not given where equations coming from injection are not yet removed, making invalid the computation of dependencies, what prevents an hypothesis to be cleared and replaced.
*	Removing "eqn:" for "induction" in reference manual.	Hugo Herbelin	2014-09-10
\|
*	Documenting the new Undo semantics	Enrico Tassi	2014-09-09
\|
*	Removing the documentation of the XML plugin.	Pierre-Marie Pédrot	2014-09-08
\|
*	Doc: [revgoals].	Arnaud Spiwack	2014-09-08
\|
*	Little fix in documentation of inversion.	Hugo Herbelin	2014-09-07
\|
*	Documenting the [Variant] type definition and the [Nonrecursive Elimination ↵	Arnaud Spiwack	2014-09-04
\| \| \| \|	Schemes] option.
*	sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex	Pierre Boutillier	2014-09-03
\|
*	Improve RefMan section about Coq_makefile	Pierre Boutillier	2014-09-03
\|
*	Update RefMan with respect to new loadpath management	Pierre Boutillier	2014-09-03
\|
*	Cbn in refman	Pierre Boutillier	2014-09-03
\|