coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fixing test-suite after last storm in Pp.	pboutill	2012-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15433 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Getting rid of Pcoq remains.	ppedrot	2012-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15432 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.	ppedrot	2012-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15431 85f007b7-540e-0410-9357-904b9bb8a0f7
*	These files are displaced from Rtrigo.v and Ranalysis_reg.v	bertot	2012-06-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15430 85f007b7-540e-0410-9357-904b9bb8a0f7
*	finish the rearrangement for removing the sin_PI2 axiom. This new version	bertot	2012-06-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- provides the atan function - shows that this function is equal between -1 and 1 to a function defined with power series - establishes the equality with the PI value as given by the alternated series constructed with PI_tg - provides a smarter theorem to compute approximations of PI, based on a formula in the same family as the one used by John Machin in 1706 Dependencies between files have been rearranged so that the new theorems are loaded with the library Reals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15429 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adds the proof of PI_ineq, plus some other smarter ways to approximate PI	bertot	2012-06-11
\| \| \| \| \| \| \|	and of course, the definition of atan (the inverse of tan, from R to (-PI/2, PI/2) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15428 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Colorization of coqtop messages is turned off by default	letouzey	2012-06-07
\| \| \| \| \| \| \| \| \| \| \| \| \|	This bling-bling feature is interacting badly with - the documentation generation - the bench logs - compilation in an emacs buffer - ... As long as these points aren't solved, no coloring by default, but on the contrary an option to manually activate it: coqtop -color git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15427 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CHANGES: mention the end of induction principles for records	letouzey	2012-06-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15426 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modifications and rearrangements to remove the action that sin (PI/2) = 1	bertot	2012-06-05
\| \| \| \| \| \|	Beware that the definition of PI changes in the process git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15425 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A box to pretty-print them all.	ppedrot	2012-06-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15424 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing previous commit (something strange happened...)	ppedrot	2012-06-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15423 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Replacing some str with strbrk	ppedrot	2012-06-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a color output to Coqtop.	ppedrot	2012-06-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15421 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Separated notice vs info messages, and cleaned up the interface a bit.	ppedrot	2012-06-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15420 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing #2803.	ppedrot	2012-06-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15419 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Forward-port fixes from 8.4 (15358, 15353, 15333).	msozeau	2012-06-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15418 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed printing error problem... A line had disappeared in a previous patch.	ppedrot	2012-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15416 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Flushing formatters before program exit.	ppedrot	2012-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15415 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More cleaning	ppedrot	2012-06-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15414 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaning Pp.ppnl use	ppedrot	2012-06-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15413 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Let's try to avoid generating induction principles for records (wish #2693)	letouzey	2012-06-01
\| \| \| \| \| \| \| \| \| \| \| \| \|	Since record cannot be recursive, induction principles for them are just wasted ressources. With this patch, we turn off there generation by default. The flag "Set/Unset Record Elimination Schemes" allows to start producing them again. For compatibility, we adapt "induction" and similar tactics that rely on the existence of induction principles : on a record, "induction" is now silently converted into "destruct". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15411 85f007b7-540e-0410-9357-904b9bb8a0f7
*	list_eq_dec now transparent (wish #2786)	letouzey	2012-06-01
\| \| \| \| \| \| \|	The proof is also replaced by a mere "decide equality". Patch by Robbert Krebbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15409 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cancel the start of a proof if its init_tac fails (fix #2799)	letouzey	2012-06-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15407 85f007b7-540e-0410-9357-904b9bb8a0f7
*	tactic is_fix, akin to is_evar, is_hyp, is_ ... family	pboutill	2012-05-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15406 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile bug for plugins	pboutill	2012-05-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15405 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Functions *_beq aren't generated anymore, remove comments about them	letouzey	2012-05-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15402 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adds Reference-Manual.out to .gitignore	letouzey	2012-05-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15401 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Getting rid of Pp.msg	ppedrot	2012-05-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More uniformisation in Pp.warn functions.	ppedrot	2012-05-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restore compatibility with camlp4 (some missing open Tok)	letouzey	2012-05-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15397 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed an error display bug in CoqIDE.	ppedrot	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15396 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Re-allow Time Back* (cf discussion on coq-club)	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15394 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Some documentation of recent changes concerning interfaces	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15393 85f007b7-540e-0410-9357-904b9bb8a0f7
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
*	place all pretty-printing files in new dir printing/	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extend become a mli-only file in intf/	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15390 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Avoid Dumpglob dependency on Lexer	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15389 85f007b7-540e-0410-9357-904b9bb8a0f7
*	No need to have Refine amongst Hightactics.cm*a	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15388 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
*	Split Egrammar into Egramml and Egramcoq	letouzey	2012-05-29
\| \| \| \| \| \| \| \|	Two gains: - no Summary in Grammar.cma - get rid of the hack concerning error_invalid_pattern_notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15386 85f007b7-540e-0410-9357-904b9bb8a0f7
*	No more Univ in grammar.cma	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15385 85f007b7-540e-0410-9357-904b9bb8a0f7
*	global_reference migrated from Libnames to new Globnames, less deps in ↵	letouzey	2012-05-29
\| \| \| \| \| \|	grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Strongly reduce the dependencies of grammar.cma, modulo two hacks	letouzey	2012-05-29
\| \| \| \| \| \| \| \| \| \| \|	- in g_constr.ml4, we avoid a dependency on Notation_ops by copying the pseudo-ident hack ldots_var = ".." - in egrammar.ml4 we duplicate the error message error_invalid_pattern_notaition. To adapt via Errors.register_handler... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15383 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15382 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Stuff about notation_constr (ex-aconstr) now in notation_ops.ml	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15381 85f007b7-540e-0410-9357-904b9bb8a0f7
*	slim down a bit genarg.ml (pr_intro_pattern forgotten there)	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15380 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Glob_term: minor formatting	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15379 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Migrate the grammar entry about "Ltac" into g_vernac.ml4.	letouzey	2012-05-29
\| \| \| \| \| \| \|	It's the right place for it, and it will allow cutting some deps for grammar.cma later. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15378 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification in deps of some g_*.ml4	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15377 85f007b7-540e-0410-9357-904b9bb8a0f7