coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Remove VernacGo	glondu	2010-10-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	I agree with Arnaud on this one... Archeology: I could trace it back to r133 (in 1999!), and it was adapted to many big changes, including change of parsing (r2722, in 2002). Maybe it was used by Centaur or something similar once... The only relevant occurrences of "Go" in SVN history (since initial commit in 1999) is that it "semble peu robuste aux erreurs", without a clear specification of what it is supposed to do... Looks like an interesting feature, though, but needs complete rethinking (and documentation) with the new engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13506 85f007b7-540e-0410-9357-904b9bb8a0f7
*	(Hopefully) clearer explanation of Ltac's context patterns	glondu	2010-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13503 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
\| \| \| \| \| \| \| \| \|	Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]". This should a priori be used with care (it might be a bit disturbing seeing the same constant used with apparently incompatible signatures). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minor fixes of 'make doc'	pboutill	2010-09-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13472 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a section in the documentation of Vernacular commands about ↵	aspiwack	2010-09-23
\| \| \| \| \| \|	Set/Unset/Test. It allowed to document the behaviour of Local and Global on Set and Unset. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13456 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Hopefully a fix for #2176 (redirection not understood with some shells)	herbelin	2010-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13437 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for ↵	emakarov	2010-09-06
\| \| \| \| \| \|	pngtopnm and pnmtops git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13401 85f007b7-540e-0410-9357-904b9bb8a0f7
*	unification des tactiques nsatz pour R Z avec celle des anneaux integres	pottier	2010-07-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13343 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minor fixes:	msozeau	2010-07-27
\| \| \| \| \| \| \| \| \|	- Document and fix [autounfold] - Fix warning about default Firstorder tactic object not being defined - Fix treatment of implicits in Program Lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13334 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of Set Automatic Coercions Import.	herbelin	2010-07-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13327 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
\| \| \| \| \| \| \| \| \| \| \| \| \|	- Added support for recursive notations with binders - Added support for arbitrary large iterators in recursive notations - More checks on the use of variables and improved error messages - Do side-effects in metasyntax only when sure that everything is ok - Documentation Note: it seems there were a small bug in match_alist (instances obtained from matching the first copy of iterator were not propagated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7
*	FSetPositive: sets of positive inspired by FMapPositive.	letouzey	2010-07-16
\| \| \| \| \| \| \| \| \| \|	Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant. I've also included a MSets version, hence FSetPositive might become soon a mere wrapper for MSetPositive, as for other FSets implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13287 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating reference manual credits: gb is now nsatz.	herbelin	2010-07-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13271 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Update of documentation for the standard library (cf. #2332)	letouzey	2010-06-28
\| \| \| \| \| \|	This is a slightly modified version of the patch proposed in #2332 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13209 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Applying François' patches about Canonical Projections (see #2302 and #2334).	herbelin	2010-06-26
\| \| \| \| \| \| \|	Printer pr_cs_pattern is kept in recordops only. Also updated CHANGES. Fixed spelling of "uniform inheritance condition" in doc too (see git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13204 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modifs de nsatz suggerees par Hugo	pottier	2010-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13194 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'une feuille de style pour les définitions spécifiques à Hevea + ↵	notin	2010-06-23
\| \| \| \| \| \|	divers corrections sur la génération du manuel de référence. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13186 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ↵	notin	2010-06-23
\| \| \| \| \| \|	coq.inria.fr) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13185 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of clear dependent and revert dependent	letouzey	2010-06-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13166 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Update of Extraction documentation	letouzey	2010-06-14
\| \| \| \| \| \| \| \| \| \| \| \|	- Removal of the notice about the "experimental" status of extraction. Of course extraction is still experimental, but no less than the rest of Coq ;-) - Removal of the example about heapsort now that Heap is obsolete. - Euclid isn't the best of the examples, but for the moment we leave it - We mention ExtrOcamlIntConv and the others extraction/*.v - Various small improvements git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13136 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction Implicit: documentation	letouzey	2010-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13133 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reverted commit 13110 about headers.sty that I wrongly thought was buggy. Sorry.	herbelin	2010-06-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13114 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed a very old (from V6.3) typo in headers.sty	herbelin	2010-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13110 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".	herbelin	2010-06-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Updated documentation in many ways: - merged binder and binderlet as done for a while in implementation - fixed a few technical problems (bad indexation of {x:A\|P x}, missing spaces in html code in many situations due to missing curly brackets around TeX macros - e.g. around \ldots -, missing dots at end of sentences, ...) - renamed "statement" commands into "assertion" commands and "declaration" commands into "assumption" commands - moved Goal and Save out of the Gallina chapter - avoid some recovering in the Gallina and proof mode chapters - slight smoothing of some hard-to-read paragraphs of the manual git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13091 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backporting part of r12970 to trunk (deprecation of double induction).	herbelin	2010-06-07
\| \| \| \| \| \|	Backport of the part of r12970 about Fixpoint doc will come in a further commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13081 85f007b7-540e-0410-9357-904b9bb8a0f7
*	doc Nstaz updated	pottier	2010-06-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13073 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A new command Compute foo, shortcut for Eval vm_compute in foo	letouzey	2010-06-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13070 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout oublie	pottier	2010-06-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13057 85f007b7-540e-0410-9357-904b9bb8a0f7
*	plugin groebner updated and renamed as nsatz; first version of the doc of ↵	pottier	2010-06-03
\| \| \| \| \| \|	nsatz in the refman git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13056 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minor fix in doc chapter on inference rules (added a missing space).	herbelin	2010-05-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13029 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extract Inductive is now possible toward non-inductive types (e.g. nat => int)	letouzey	2010-05-21
\| \| \| \| \| \| \| \| \| \| \|	For instance: Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n => if n=0 then fO () else fS (n-1))". See Extraction.v for more details and caveat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13025 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove compile-command pragmas for emacs	letouzey	2010-05-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	These declarations (e.g. make -C .. bin/coqtop.byte) are quite annoying when debugging stuff over the whole archive: all of a sudden, M-x recompile isn't doing what you intended just because you've visited some specific files. Instead: - Feel free to rather add intermediate targets in the Makefile if they aren't there yet. - For avoiding typing the -C with many .. after, you can have a look at my recursively-descending make: http://www.pps.jussieu.fr/~letouzey/download/make.sh which is to be renamed make and placed in a bin dir with more priority than /usr/bin. Beware! I've already add a few bad surprises with this hack, but it's really convenient nonetheless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13014 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Some ocamldoc comments + Fixing name of .coqrc.version file in refman	pboutill	2010-05-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13013 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Update of credits files	herbelin	2010-05-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13004 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction in Function documentation	jforest	2010-05-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12995 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
\| \| \| \| \| \| \| \| \| \| \|	- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
*	small detail about Scheme Equality	vsiles	2010-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12966 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Applying François Garillot's patch (#2261 in bug tracker) for extended	herbelin	2010-04-22
\| \| \| \| \| \| \|	syntax of "Implicit Type" (that can now be "Implicit Types" and can now accept several blocks of variables of a given type). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12960 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documenting the use of ##, %%, $$ in coqdoc.	herbelin	2010-04-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12909 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Applied Cédric Auger's patch to fix use of "#&xxx;" in html printing	herbelin	2010-04-09
\| \| \| \| \| \| \| \| \| \| \| \|	rules (bug report #2293). Restored the sequential extension of the printing rules tables (that commit #12905 replaced by a per-file modification of the printing rules table). Note however that the table grows in the order of compilation of files by coqdoc, which does not necessarily coincide with the order of coqc compilation dependencies of the files. Added documentation of coqdoc option "--external". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12908 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add documentation on the treatment of [if] and [let (x1, ... xn) := ..]	msozeau	2010-03-31
\| \| \| \| \| \| \| \|	by Program. Fix some broken examples and detail the syntax of order annotations for well-founded recursion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12897 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Update manual on search commands	puech	2010-03-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12861 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #2214 + maj liens web	notin	2010-02-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12815 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Polishing the setup of CoqIDE Input Method	vgross	2010-02-18
\| \| \| \| \| \| \| \|	autodetection via ./configure, automated installation target "install-im", and no more patching. Plus documentation of the procedure in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12790 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of the ! annotation for functor application	letouzey	2010-02-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12746 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau	2010-02-10
\| \| \| \| \| \| \|	dependency order of obligations that was not backwards-compatible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12719 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Update CHANGES, add documentation for new commands/tactics and do a bit	msozeau	2010-01-30
\| \| \| \| \| \| \|	of cleanup in tactics/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12705 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New command Declare Reduction <id> := <conv_expr>.	letouzey	2010-01-28
\| \| \| \| \| \| \| \|	Let's avoid writing huge "Eval ... in ..." lines :-) Will be used in particular soon in NMake for defining function via Definition ... := Eval ... in ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12699 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Document Local Declare ML Module	glondu	2010-01-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12674 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Include can accept both Module and Module Type	letouzey	2010-01-07
\| \| \| \| \| \| \| \|	Syntax Include Type is still active, but deprecated, and triggers a warning. The syntax M <+ M' <+ M'', which performs internally an Include, also benefits from this: M, M', M'' can be independantly modules or module type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7