coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	SetoidList: explicit the fact that InfA_compat won't use ltA_strorder	letouzey	2012-05-22
\| \| \| \| \| \| \| \|	For that, we use the new "Proof using ...". This way, we're sure that a later change in the behavior of intuition or any other tactics will not create an artificial dependency again (cf. r15180). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15340 85f007b7-540e-0410-9357-904b9bb8a0f7
*	List + Permutation : more results about nth_error and nth	letouzey	2012-05-18
\| \| \| \| \| \| \| \| \| \|	In particular, characterisation of NoDup and Permutation in term of nth_error and nth Some of these results have been suggested last year by Bas Spitters (cf. MathClasses). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15336 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed bug #2781... (We hope so.)	ppedrot	2012-05-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15335 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Trying to fix bug #2780, by short-circuiting the Gtk signals. A bit hackish.	ppedrot	2012-05-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15334 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide: make some paths win32-compliant	letouzey	2012-05-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15332 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revert commit 15287 : the env variables are indeed access at launch-time	letouzey	2012-05-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15331 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intuition: temporary(?) restore the unconditional unfolding of not	letouzey	2012-05-15
\| \| \| \| \| \| \| \|	Let's check tomorrow the impact on contribs: are the recent build failures related to the "not" unfolding stategy or to the new handling of conjonction-like constructors ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15330 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide: minor formatting improvement of an error message	letouzey	2012-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15329 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide: in win32 command given to cmd.exe should be more quoted	letouzey	2012-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15328 85f007b7-540e-0410-9357-904b9bb8a0f7
*	when cross-compiling with mingw32, let's fix the Filename.dir_sep	letouzey	2012-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15327 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: Really avoid locales in $(DATE)	letouzey	2012-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15326 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide: display initial connection errors in popups instead of on stderr	letouzey	2012-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15325 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Notations are back in the "in" clause of pattern matching.	pboutill	2012-05-15
\| \| \| \| \| \|	Fixes the test-suite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15324 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added semantic completion in CoqIDE. (Should also add an option for that...)	ppedrot	2012-05-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15317 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tweaking options of CoqIDE.	ppedrot	2012-05-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15316 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Some cosmetic changes w.r.t. the previous commit.	ppedrot	2012-05-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15315 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Heavily rewritten the coqtop management process of coqide. The coqtop	ppedrot	2012-05-13
\| \| \| \| \| \| \| \| \| \|	object is now responsible for restarting itself, and handles unexpected crashes. Fixes a lot of errors in file descriptor management, but may introduce lurking deadlocks and nasty bugs waiting to be discovered. Only (quickly) tested under Linux, any callbacks from Windows are welcome. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15314 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a SearchAbout-like primitive in coqtop interface.	ppedrot	2012-05-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15313 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added an interface primitive to ask coqtop for its internal versions.	ppedrot	2012-05-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15312 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Vectors takes advantage of pattern matching compiler fixup	pboutill	2012-05-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15308 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Impossible branches inference fixup (bug 2761)	pboutill	2012-05-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15307 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile.build typo in echo	pboutill	2012-05-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15306 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Slightly modified the coqtop interface by adding an identifier in	ppedrot	2012-05-11
\| \| \| \| \| \|	goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15303 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tentative and very experminental support for typerex. Enabled with	aspiwack	2012-05-11
\| \| \| \| \| \| \| \| \| \| \| \|	./configure -typerex . It causes (non-fatal) errors when compiling files without a .mli (the problem seems to have something to do with the flag -intf-suffix .cmi). In practice, most typerex functionalities don't work well because typerex fails its lookup into files compiled with -rectypes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15302 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide awful coqtop options parsing fixup	pboutill	2012-05-11
\| \| \| \| \| \|	(back to the future) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15301 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
*	Little bit of code refactoring in CoqIDE	ppedrot	2012-05-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15292 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug 2767	pboutill	2012-05-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15291 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tactic unfold always asks for comma between names.	pboutill	2012-05-09
\| \| \| \| \| \|	Else the parser takes "at" as a constant to unfold in "unfold plus at ...". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15290 85f007b7-540e-0410-9357-904b9bb8a0f7
*	End of Gtksourceview switch clean.	pboutill	2012-05-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15289 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing dead code in CoqIDE made useless by the GtkSourceView switch.	ppedrot	2012-05-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15288 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed access to environment variables in CoqIDE. Up to now, those	ppedrot	2012-05-08
\| \| \| \| \| \|	variables where set at compile time... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15287 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
*	Rewritten the autocompletion mechanism of CoqIDE, and stuffed it	ppedrot	2012-05-08
\| \| \| \| \| \| \| \|	into the ScriptView widget. The autocompletion algorithm may be a bit too greedy, so there are tests to do on huge buffers to check whether it is too slow and therefore we should fine-tune it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15282 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleanly rewritten the undo manager, which did not support redo and had	ppedrot	2012-05-06
\| \| \| \| \| \| \|	a lot of deprecated code. Trying to be nicer with the built-in undo manager of GtkSourceView btw. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15281 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renamed Undo to conform to CoqIDE widget naming convention. In addition,	ppedrot	2012-05-05
\| \| \| \| \| \| \|	made various hack to handle GtkSourceView built-in undo/redo and made method types and names more compliant with the one of Gtk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15280 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Hack to handle trailing whitespace display in CoqIDE	ppedrot	2012-05-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15279 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
*	Added a bunch of new options relative to editor.	ppedrot	2012-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15274 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Better style handling in CoqIDE	ppedrot	2012-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15273 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed previous commit	ppedrot	2012-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15272 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removed the useless use of a reference in preference handling.	ppedrot	2012-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15271 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Quick workaround to handle badly designed Sourceview package.	ppedrot	2012-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15270 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide highligthing is back (done by gtksourceview).	pboutill	2012-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15269 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide coq lexer put one tag at the end of a sentence.	pboutill	2012-05-02
\| \| \| \| \| \| \|	And that's all ! It erase the possibility of code folding... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15268 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Source language and style are preferences	pboutill	2012-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15267 85f007b7-540e-0410-9357-904b9bb8a0f7
*	undoable_view is a source_view	pboutill	2012-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15266 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Always add the Coq_config.dirs to xdg_dirs	pboutill	2012-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15265 85f007b7-540e-0410-9357-904b9bb8a0f7