coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	make sure that documentation compilation works after adding files for	bertot	2012-06-12
\| \| \| \| \| \|	arc tangent and computations of PI approximations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15436 85f007b7-540e-0410-9357-904b9bb8a0f7
*	place all files specific to camlp4 syntax extensions in grammar/	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed #2789.	ppedrot	2012-05-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15360 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Addedum to documentation of bullets: I now use the dedicated coq_example	aspiwack	2012-05-10
\| \| \| \| \| \|	environment to display the example. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15295 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation for Unfocused, braces and bullets.	aspiwack	2012-05-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15293 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rephrasing section on Sorts in CIC chapter, accordingly to discussions	herbelin	2012-05-08
\| \| \| \| \| \|	with Assia and Guillaume. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15284 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ref. man., ch. CIC: clarifying the redundancy coming from having both	herbelin	2012-05-08
\| \| \| \| \| \|	Prop <= Type(i) and the conjunction of Prop <= Set and Set <= Type(i). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15283 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixup r15251 second time	pboutill	2012-05-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15275 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removed the quasi-useless gtk2rc file and the documentation that went with ↵	ppedrot	2012-04-27
\| \| \| \| \| \|	it. Now CoqIDE is not anymore totally irrespectful of the local configuration of themes, in particular w.r.t. to menu fonts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15251 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MSetRBT : implementation of MSets via Red-Black trees	letouzey	2012-04-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Initial contribution by Andrew Appel, many ulterior modifications by myself. Interest: red-black trees maintain logarithmic depths as AVL, but they do not rely on integer height annotations as AVL, allowing interesting performance when computing in Coq or after standard extraction. More on this topic in the article by A. Appel. The common parts of MSetAVL and MSetRBT are shared in a new file MSetGenTree which include the definition of tree and functions such as mem fold elements compare subset. Note that the height of AVL trees is now the first arg of the Node constructor instead of the last one. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15168 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation in the documentation: remove the use of 'coinductive' in	aspiwack	2012-04-13
\| \| \| \| \| \|	favour of 'co-inductive'. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15162 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of records defined with the keywords Inductive and	aspiwack	2012-04-13
\| \| \| \| \| \|	CoInductive. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15161 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restores pdf bookmarks in the reference manual.	aspiwack	2012-04-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15160 85f007b7-540e-0410-9357-904b9bb8a0f7
*	lib directory is cut in 2 cma.	pboutill	2012-04-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Slight change in the semantics of arguments scopes: scopes can no	herbelin	2012-03-26
\| \| \| \| \| \| \| \| \| \| \|	longer be bound to Funclass or Sortclass (this does not seem to be useful). [An exception is when using modules, if a constant foo is expanded into a type, a "Bind Scope sc with foo" starts binding Sortclass]. Also reworked reference manual for Arguments Scopes and Bind Scopes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15098 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of last commit concerning Backtracking	letouzey	2012-03-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15086 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove old proof-managment commands Suspend/Resume	letouzey	2012-03-23
\| \| \| \| \| \| \|	There're not compatible with the current Backtrack mecanism used both by ProofGeneral and CoqIDE. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15083 85f007b7-540e-0410-9357-904b9bb8a0f7
*	RefMan: Environment variables description update	pboutill	2012-03-19
\| \| \| \| \| \|	There is no mention in the refman of relative search of the lib from the binaries directory and of the use of _CoqProject by CoqIdE. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15052 85f007b7-540e-0410-9357-904b9bb8a0f7
*	RefMan update about match syntax.	pboutill	2012-02-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15002 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- changing minimal version for OCaml: Coq uses Filename.dirsep that is ↵	notin	2012-02-20
\| \| \| \| \| \| \| \|	available from OCaml 3.11.2 (see bug #2707) - fixing outdated address for Coq Club git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14987 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Document the [unify] tactic.	msozeau	2012-02-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14984 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation for Grab Existential Variables.	aspiwack	2012-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14974 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrected a careless cut-and-paste in Gallina description which dated back ↵	ppedrot	2012-02-01
\| \| \| \| \| \|	to 2003. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14963 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Improved synchronisation of stdlib index page with current library state.	herbelin	2012-02-01
\| \| \| \| \| \| \| \| \| \|	- Made generation of index page fail if a file is missing in list or listed but unbound in existing theories - Added a file hidden-files to optionally list library files not to show in the index page (though it is currently empty) - Added directory Unicode (why not to have it after all?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14957 85f007b7-540e-0410-9357-904b9bb8a0f7
*	index-list.html.template: add missing files	pboutill	2012-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14955 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqtop and coqc: cleaning description of options in RefMan and manpages.	pboutill	2012-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14934 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added documentation for "r foo" in Ltac debugger.	herbelin	2012-01-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14931 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added documentation for "Set Parsing Explicit" + fixed mistakenly	herbelin	2012-01-20
\| \| \| \| \| \|	committed "assert" in commit r14928. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14930 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added the btauto tactic to the documentation.	ppedrot	2012-01-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14921 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).	herbelin	2011-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14864 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Version number, copyright, credits: missing updates.	herbelin	2011-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14862 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Credits for 8.4: More exhaustive list of external contributors.	herbelin	2011-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14852 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Credits for 8.4 + resetting COMPATIBILITY file.	herbelin	2011-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14846 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed a Not_found bug when declaring in a section some implicit	herbelin	2011-12-18
\| \| \| \| \| \| \| \| \|	arguments for a constant not defined in the section. Also fixed some typos in the doc of implicit arguments in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14816 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Command Arguments: standardizing format of error messages and American spelling.	herbelin	2011-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14810 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Proof using ...	gareuselesinge	2011-12-12
\| \| \| \| \| \| \| \| \| \| \| \| \|	New vernacular "Proof using idlist" to declare the variables to be discharged at the end of the current proof. The system checks that the set of declared variables is a superset of the set of actually used variables. It can be combined in a single line with "Proof with": Proof with .. using .. Proof using .. with .. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Html page titles	pboutill	2011-12-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14774 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of Arguments + implicits	gareuselesinge	2011-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14769 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation for Arguments + notation scopes	gareuselesinge	2011-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14768 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation for Arguments + simpl	gareuselesinge	2011-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14767 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bugs in doc about when "with" is needed or not to give bindings	herbelin	2011-12-04
\| \| \| \| \| \|	to tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of appcontext	letouzey	2011-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14744 85f007b7-540e-0410-9357-904b9bb8a0f7
*	doc: two minor fixes to make my latex happy	letouzey	2011-11-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14733 85f007b7-540e-0410-9357-904b9bb8a0f7
*	/home/pirbo/.coqrc* are read again	pboutill	2011-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14714 85f007b7-540e-0410-9357-904b9bb8a0f7
*	-user option removal	pboutill	2011-11-21
\| \| \| \| \| \| \|	it is imcompatible with the freedesktop policy that config directory is private. Feel absolutly free to revert this commit if you think -user should stay git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14713 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqrc in the right XDG_CONFIG_HOME/coq folder	pboutill	2011-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14696 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIdE configuration file won't pollute your home anymore	pboutill	2011-11-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14694 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add support for XDG_DATA_HOME and XDG_DATA_DIRS.	pboutill	2011-11-20
\| \| \| \| \| \|	From Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14692 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction.tex: typo in an Extract Inductive example (fix #2625)	letouzey	2011-10-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14574 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mainbiblio.bib : get rid of merge marker from failed merge	letouzey	2011-10-09
\| \| \| \| \| \|	Thanks to Tom Prince for spotting this git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14530 85f007b7-540e-0410-9357-904b9bb8a0f7