coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey	2012-07-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Suppose we declare : Notation foo := bar (compat "8.3"). Then each time foo is used in a script : - By default nothing particular happens (for the moment) - But we could get a warning explaining that "foo is bar since coq > 8.3". For that, either use the command-line option -verb-compat-notations or the interactive command "Set Verbose Compat Notations". - There is also a strict mode, where foo is forbidden : the previous warning is now an error. For that, either use the command-line option -no-compat-notations or the interactive command "Unset Compat Notations". When Coq is launched in compatibility mode (via -compat 8.x), using a notation tagged "8.x" will never trigger a warning or error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
\| \| \| \| \| \| \| \| \|	Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15368 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Vernacexpr is now a mli-only file, locality stuff now in locality.ml	letouzey	2012-05-29
\| \| \| \| \| \|	Adds a directory ./intf for pure interfaces. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revert copy/pasted function in to minilib thanks to clib.cma	pboutill	2012-05-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 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
*	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
*	Added an interface call to exit Coqtop nicely.	ppedrot	2012-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15263 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Implicit arguments of Definition are taken from the type when given by the user.	pboutill	2012-04-27
\| \| \| \| \| \|	There is a warning if the term is more precise. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15252 85f007b7-540e-0410-9357-904b9bb8a0f7
*	migrate g_obligations.ml4 in parsing	letouzey	2012-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15248 85f007b7-540e-0410-9357-904b9bb8a0f7