coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fixes a bug in Ppvernac which had braces and bullets printed with an ending	aspiwack	2012-07-04
\| \| \| \| \| \|	period. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15509 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Change how the number of open goals is printed.	aspiwack	2012-07-04
\| \| \| \| \| \| \| \| \| \|	If you are focused on 3 subgoals, and unfocusing would reveal 2 extra subgoals, and unfocusing again would reveal 4 extra subgoals, then coqtop will tell you: 3 focused subgoals (unfocused: 2-4) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15508 85f007b7-540e-0410-9357-904b9bb8a0f7
*	When focused on an empty list of goal (after finishing a subproof introduced	aspiwack	2012-07-04
\| \| \| \| \| \| \|	by a bullet or a brace, for instance), the message "This subproof is complete […]" is now rendered before the list of goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15507 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Various small display improvement	ppedrot	2012-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15505 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reversed message display order in CoqIDE	ppedrot	2012-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15504 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Small improvement to ide_slave, which was going crazy whenever	ppedrot	2012-06-29
\| \| \| \| \| \|	stdin was accidentaly closed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15503 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing fake_ide	ppedrot	2012-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15502 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Now CoqIDE separates answer and messages. This should hopefully	ppedrot	2012-06-29
\| \| \| \| \| \|	be backward compatible... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15501 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaning opening of the standard List module.	ppedrot	2012-06-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15500 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Replace nat indices with positive one in Btauto.	ppedrot	2012-06-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15499 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing previous commit.	ppedrot	2012-06-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15498 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing info_auto / info_trivial display.	ppedrot	2012-06-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15497 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added the show_margin_right option to CoqIDE	ppedrot	2012-06-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15496 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing awkward copy & paste mechanism in CoqIDE.	ppedrot	2012-06-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15495 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Now CoqIDE auto-sets the printing width of the goal display.	ppedrot	2012-06-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15494 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed string width printing in string_of_ppcmds	ppedrot	2012-06-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15493 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a Deque module to CLib (to be used in CoqIDE).	ppedrot	2012-06-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15492 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Small code compaction and factoring in CoqIDE.	ppedrot	2012-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15491 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a .mli to pretyping/program.ml	ppedrot	2012-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15490 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cosmetic changes	ppedrot	2012-06-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15489 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Made the message view of CoqIDE abstract.	ppedrot	2012-06-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15488 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of pp.mli	ppedrot	2012-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15487 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moving logging level to Interface.	ppedrot	2012-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15486 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed cursor reset in CoqIDE backtrack.	ppedrot	2012-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15485 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Factorized bactracking code in CoqIDE. This fixes bug #2821 btw.	ppedrot	2012-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15484 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing a potential bug of coqtop management in CoqIDE due to a	ppedrot	2012-06-23
\| \| \| \| \| \|	careless exception catching. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15483 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing Camlp4 compilation (hopefully, preprocessing fixpoint reached...)	ppedrot	2012-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15482 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing camlp4 compilation w.r.t previous commit	ppedrot	2012-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15481 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: make uninstall target	pboutill	2012-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15480 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Install is rather beautiful	pboutill	2012-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15479 85f007b7-540e-0410-9357-904b9bb8a0f7
*	inthe middle one more time	pboutill	2012-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15478 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Refactoring seems OK	pboutill	2012-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15477 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: separate finding what to install where from generating the ↵	pboutill	2012-06-22
\| \| \| \| \| \|	script that install git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15476 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
\| \| \| \| \| \| \| \| \| \|	were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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