coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	I forgot a line in previous commit.	aspiwack	2012-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15473 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A call to the command Proof (and its variants) now prints the subgoals.	aspiwack	2012-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15472 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed #2821.	ppedrot	2012-06-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15471 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing #2825.	ppedrot	2012-06-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug #2808: wrong handling of evars in Instance command.	msozeau	2012-06-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15468 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug #2791 by doing a fixpoint computation in consider_remaining_problems:	msozeau	2012-06-21
\| \| \| \| \| \| \|	take care of checking progress when solving the remaining problems, distinguishing between solved and stuck conversions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15467 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing accelerator dynamic modification in CoqIDE.	ppedrot	2012-06-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15465 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing use of an error instead of a boolean result in the unification	herbelin	2012-06-20
\| \| \| \| \| \| \| \|	subroutine choose_less_dependent_instance. This might solve bug #2495 (only "might solve" because the bug does not come with a reproducible example). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15461 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bug #2817 (occur check was not done up to instantiation of	herbelin	2012-06-20
\| \| \| \| \| \|	known instances in unification.ml). This refines the fix to bug #1918. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15459 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bug #2809 (anomaly when printing a module with notations due to	herbelin	2012-06-20
\| \| \| \| \| \| \|	bad interaction between lazy evaluation of pp streams and temporary effectful extension of global environment). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15457 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Install compat5 module with grammar.cma	pboutill	2012-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15456 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug 2813 - Reflexive, Symmetric, Transitive instances for pointwise_relation ↵	pboutill	2012-06-20
\| \| \| \| \| \|	patch git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15455 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug 2823: update INSTALL.ide in order to ask for lablgtksourceview	pboutill	2012-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15454 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug #2790: wrong handling of Set -> Prop -> Prop products in setoid ↵	msozeau	2012-06-19
\| \| \| \| \| \|	rewriting. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15452 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug #2695: infinite loop in dependent destruction.	msozeau	2012-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15451 85f007b7-540e-0410-9357-904b9bb8a0f7
*	BinInt: a forgotten scope for a notation	letouzey	2012-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15450 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing printing of @f with no arguments	herbelin	2012-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15448 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing some inconsistencies of constr printer wrt constr parser	herbelin	2012-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15447 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Proof using: nested sections bugfix	gareuselesinge	2012-06-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	It used to be the case that the list of declared section variables for a constant was taken into account only when discharging the first enclosing sections, but not any outer section. Example of the bug: Section A. Variable x : bool. Section B. Variable y : nat. Lemma foo : True. Proof using x y. Admitted. End B. End A. Check foo. (* nat -> True instead of bool -> nat -> True *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15445 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reductionops abstract machine uses Zcase & Zfix stack node.	pboutill	2012-06-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15444 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reductionops : Better abstract machine stack utilities	pboutill	2012-06-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15443 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix coqide vernac lexer	pboutill	2012-06-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15442 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Partialy revert "coq_makefile fixup" because old Makefiles still need CAMLP4BIN	pboutill	2012-06-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15441 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Constrextern is allow to use partially applied notations	pboutill	2012-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15440 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Internalization of pattern is done in two phases.	pboutill	2012-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	First Notations, syntactic definitions, primitive entries are tackled to build raw_cases_pattern_expr. Reference are revolved at this time too. Then raw_patterns are internalized as cases_pattern or applied inductive (dealing with implicit args, or_pattern refactoring, aliases). It is more uniform, it allows notations for non fully applied constructors but : - It does not raise a warning when an identifier is also a global_reference different than a constructor. - It looks for implicit arguments twice. (because finding scopes of arguments asks for implicit arguments). - It does not deal anymore with constants that evaluates to constructor. (This one is voluntary, dealing with implicit & notations is already a hell full of bugs so what will be next step ? Any terms that computes to a pattern ???) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15439 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coq_makefile fixup	pboutill	2012-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15438 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing annoying autocompletion when deleting text.	ppedrot	2012-06-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15437 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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
*	New step in purpose to get both camlp4 and camlp5 compatible coq_makefiles	pboutill	2012-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15435 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug 2805: Only export CAMLP4LIB if camlp4 -where ends successfully	pboutill	2012-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15434 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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