coq - The formal proof system

Age	Commit message (Expand)	Author
2011-06-30	Keep obligation source information in Program	msozeau
2011-06-21	Cleaning debugging printer relative to new proof engine. In	herbelin
2011-06-20	Add compatibility option "-compat 8.3".	herbelin
2011-06-18	Relaxed the constraint introduced in r14190 that froze the existing	herbelin
2011-06-14	Fixing bug #2181 (Class mechanism can create dependencies over unnamed	herbelin
2011-06-13	Another bug of Scheme Induction (generated names dep/nodep were swapped).	herbelin
2011-06-13	Fixing an anomaly in Scheme Induction.	herbelin
2011-05-24	Made the emacs-U option deprecated. Also removed the old code	courtieu
2011-05-18	Coqide: allow the use of Abort (grant wish #2357)	letouzey
2011-05-17	More work on error handling	letouzey
2011-05-17	Break circular dependency Proof_global -> Vernacexpr -> Proof_global.	aspiwack
2011-05-16	Repair the "Fail" command after recent changes in exception handling	letouzey
2011-05-16	turn the automatic generation of boolean equality	vsiles
2011-05-15	Turning Sys_error into error by default instead of anomaly. After all,	herbelin
2011-05-13	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-11	Print Module (Type) M now tries to print more details	letouzey
2011-05-05	Merge branch 'subclasses' into coq-trunk	msozeau
2011-04-29	Fixed a bug causing inconsistent states during proof editting.	aspiwack
2011-04-28	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-21	Coqide: better handling of stdout/stderr in win32	letouzey
2011-04-18	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau
2011-04-14	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-13	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-08	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-06	Add 'Existing Instances' declaration to declare multiple instances at once.	letouzey
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2011-03-30	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-28	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-25	Ide_intf : change type of location in ide	letouzey
2011-03-23	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-17	An option "Set Default Timeout n."	letouzey
2011-03-17	Goptions: repair Unset for int options	letouzey
2011-03-16	Finish branching functions handling module errors (cf. r13886)	letouzey
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
2011-03-11	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-07	Reverted commit r13893 about propagation of more informative	herbelin