coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	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
*	Specific syntax for Instances in Module Type: Declare Instance	letouzey	2010-01-04
\| \| \| \| \| \| \| \| \|	NB: the grammar entry is placed in vernac:command on purpose even if it should have gone into vernac:gallina_ext. Camlp4 isn't factorising rules starting by "Declare" in a correct way otherwise... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12623 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Patches and instructions to enable Input Method support in CoqIDE.	vgross	2009-12-21
\| \| \| \| \| \| \|	TODO: don't patch the ELatin IM, create a separate IM or push the patch upstream. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12604 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Description of the new features of the module system (part two).	soubiran	2009-12-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12588 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Description of the new features of the module system (first part).	soubiran	2009-12-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12587 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Document Generalizable Variables, and change syntax to	msozeau	2009-11-15
\| \| \| \| \| \| \| \| \|	[Generalizable (All\|No) Variables (ident+)?], also update type classes documentation to reflect the latest changes in instance decls. Fix a bug in [Util.list_split_when]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12525 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added support for multiple where-clauses in Inductive and co (see wish #2163).	herbelin	2009-11-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12500 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Cleaning and uniformisation in command.ml: - For better modularity and better visibility, two files got isolated out of command.ml: - lemmas.ml is about starting and saving a proof - indschemes.ml is about declaring inductive schemes - Decomposition of the functions of command.ml into a functional part and the imperative part - Inductive schemes: - New architecture in ind_tables.ml for registering scheme builders, and for sharing and generating on demand inductive schemes - Adding new automatically generated equality schemes (file eqschemes.ml) - "_congr" for equality types (completing here commit 12273) - "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep", "_rew_backward" (similar to eq_rect), "_rew_backward_dep" for rewriting schemes (warning, rew_forward_dep cannot be stated following the standard Coq pattern for inductive types: "t=u" cannot be the last argument of the scheme) - "_case", "_case_nodep", "_case_dep" for case analysis schemes - Preliminary step towards discriminate and injection working on any equality-like type (e.g. eq_true) - Restating JMeq_congr under the canonical form of congruence schemes - Renamed "Set Equality Scheme" into "Set Equality Schemes" - Added "Set Rewriting Schemes", "Set Case Analysis Schemes" - Activation of the automatic generation of boolean equality lemmas - Partial debug and error messages improvements for the generation of boolean equality and decidable equality - Added schemes for making dependent rewrite working (unfortunately with not a fully satisfactory design - see file eqschemes.ml) - Some names of ML function made more regular (see dev/doc/changes.txt) - Incidentally, added a flush to obsolete Local/Global syntax warning git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio	2009-11-04
\| \| \| \| \| \| \|	Fixed pretty printing of record syntax. Allowed record syntax inside patterns. (Patch by Cedric Auger.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removed 'Toplevel' language from extraction documentation, since it is not ↵	gmelquio	2009-11-04
\| \| \| \| \| \|	currently supported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12467 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Report de la révision #12208 de la v8.2 (correction du bug #2126)	notin	2009-11-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12466 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #2175	notin	2009-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12456 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed some typos in the reference manual.	gmelquio	2009-10-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12443 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo in the refman	puech	2009-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12433 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of the Local and Global modifiers.	herbelin	2009-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12425 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix Setoid documentation.	msozeau	2009-10-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12421 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New cleaning phase of the Local/Global option management	herbelin	2009-10-26
\| \| \| \| \| \| \| \| \|	- Clarification and documentation of the different styles of Local/Global modifiers in vernacexpr.ml - Addition of Global in sections for Open/Close Scope. - Addition of Local for Ltac when not in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Improved the treatment of Local/Global options (noneffective Local on	herbelin	2009-10-25
\| \| \| \| \| \| \| \| \| \| \| \|	Implicit Arguments, Arguments Scope and Coercion fixed, noneffective Global in sections for Hints and Notation detected). Misc. improvements (comments + interpretation of Hint Constructors + dev printer for hint_db). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7