coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Made the emacs-U option deprecated. Also removed the old code	courtieu	2011-05-24
*	Coqide: allow the use of Abort (grant wish #2357)	letouzey	2011-05-18
*	More work on error handling	letouzey	2011-05-17
*	Break circular dependency Proof_global -> Vernacexpr -> Proof_global.	aspiwack	2011-05-17
*	Repair the "Fail" command after recent changes in exception handling	letouzey	2011-05-16
*	turn the automatic generation of boolean equality	vsiles	2011-05-16
*	Turning Sys_error into error by default instead of anomaly. After all,	herbelin	2011-05-15
*	A new mechanism to handle errors.	aspiwack	2011-05-13
*	New option [Set Bullet Behavior] allows to select the behaviour of bullets.	aspiwack	2011-05-13
*	Print Module (Type) M now tries to print more details	letouzey	2011-05-11
*	Merge branch 'subclasses' into coq-trunk	msozeau	2011-05-05
*	Fixed a bug causing inconsistent states during proof editting.	aspiwack	2011-04-29
*	coqtop -config returns coq returns coq environments at exection time	pboutill	2011-04-28
*	Fixed notation printing bug when curly brackets are involved (requests	herbelin	2011-04-28
*	Coqide: better handling of stdout/stderr in win32	letouzey	2011-04-21
*	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau	2011-04-18
*	Add directories in COQPATH to search path.	herbelin	2011-04-14
*	Reorder search path order, so the standard library is search last.	herbelin	2011-04-14
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	- Make typeclass transparency information directly available	msozeau	2011-04-13
*	- Remove create_evar_defs	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Replaced printing number of ill-typed branch by printing name of constructor	herbelin	2011-04-08
*	Fixed "Eval ... in t" when t has still metavariables.	herbelin	2011-04-08
*	Add 'Existing Instances' declaration to declare multiple instances at once.	letouzey	2011-04-06
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Ide_intf: documentation of calls + debug printing of calls/answers	letouzey	2011-03-30
*	Ide_intf: remove useless int answer to the "interp" and "rewind" calls	letouzey	2011-03-30
*	Ide_slave: better handling of Ctrl-C	letouzey	2011-03-30
*	Ide_slave : fix last commit, use ad_hoc catch_break instead of Sys.catch_break	letouzey	2011-03-28
*	Ide_slave: improved handling of exceptions (in particular ^C)	letouzey	2011-03-28
*	Ide_slave: a more robust current_status () function	letouzey	2011-03-28
*	Ide_intf : change type of location in ide	letouzey	2011-03-25
*	Ide: stronger separation from coqtop	letouzey	2011-03-23
*	Ide: experimentally allow coqide to interrupt or kill coqtop	letouzey	2011-03-23
*	- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...	msozeau	2011-03-23
*	An option "Set Default Timeout n."	letouzey	2011-03-17
*	Goptions: repair Unset for int options	letouzey	2011-03-17
*	Finish branching functions handling module errors (cf. r13886)	letouzey	2011-03-16
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Keep information on which fields are subclasses in class declarations,	msozeau	2011-03-11
*	- Better error messages taking unif. constraints into account.	msozeau	2011-03-11
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	Added a table for using reserved names for binding names to types	herbelin	2011-03-05
*	Moving printing of module typing errors upwards to himsg.ml so as to	herbelin	2011-03-05
*	A few more betaiota on environments and types of error messages. Seems to	herbelin	2011-03-05
*	Filter out admitted subgoals from search results	glondu	2011-02-25
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	An automatic substitution of scope at functor application	letouzey	2011-02-11