coq - The formal proof system

Age	Commit message (Expand)	Author
2013-03-21	Robust display of NotConvertibleTypeField errors (fix #3008, #2995)	letouzey
2013-03-21	Firstorder: record with defined field aren't conjonctions (fix #2629)	letouzey
2013-03-21	Using hnf instead of "intro H" for forcing reduction to a product.	herbelin
2013-03-21	Fixing an old pecularity of "red": head betaiota redexes are now	herbelin
2013-03-21	Typo dans message d'erreur (obligations).	herbelin
2013-03-21	Add type information in error message when a constructor is not fully	herbelin
2013-03-21	Check unexpected "Local" keyword in cmd before opening a proof (fix #2975)	letouzey
2013-03-21	Removing mandatory suffixes for library files.	ppedrot
2013-03-21	Printmod: handle more examples thanks to better nametab use	letouzey
2013-03-21	Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)	letouzey
2013-03-20	Check a list length before doing a List.chop (fix #3000)	letouzey
2013-03-20	Better encapsulation of MessageView	ppedrot
2013-03-19	Using ML signalling in CoqIDE	ppedrot
2013-03-19	Adding color for warnings in CoqIDE	ppedrot
2013-03-19	Removing the module Libtypes and unifying the Search[Pattern\|Rewrite]?	ppedrot
2013-03-18	Fix for bug #3004 (thanks Hugo!)	letouzey
2013-03-18	Extraction AccessOpaque is now activated again by default (#2952)	letouzey
2013-03-18	Making local variable warning verbose by default.	ppedrot
2013-03-17	Ppvernac: no globalization for printing ltac definitions	letouzey
2013-03-17	Fix some camlp5 quotations , restoring compatibility with camlp5 5.x	letouzey
2013-03-17	Checker: simplify a bit its exception handler	letouzey
2013-03-17	Avoid a few overzealous "when Errors.noncritical"	letouzey
2013-03-17	Retyping.get_type_of: a lax version raising no anomalies	letouzey
2013-03-16	another Errors.push in a exception reraise	letouzey
2013-03-15	Extract_env : correct exceptions mentionned in a try ... with	letouzey
2013-03-14	Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical	letouzey
2013-03-14	Cerrors: get rid of some FIXME	letouzey
2013-03-14	Typo in an error message	letouzey
2013-03-14	Use Pp.msg instead of Pp.pp in -beautify (loss of text otherwise)	letouzey
2013-03-14	Pptactic.pr_raw_tactic is now without env argument	letouzey
2013-03-13	Modules and ppvernac, sequel of Enrico's commit 16261	letouzey
2013-03-13	Declaremods: a few syntactic improvements	letouzey
2013-03-13	Made the backtrace type opaque	ppedrot
2013-03-13	Fix compilation of coqchk (broken by commit 16268), bis repetita	letouzey
2013-03-13	Fix compilation of coqchk (broken by commit 16268)	letouzey
2013-03-13	Toplevel: improved comments	letouzey
2013-03-13	Vernac+Toplevel: get rid of Error_in_file	letouzey
2013-03-13	Vernac+Toplevel: get rid of DuringVernacInterp	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 15)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 14)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 13)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 11)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 10)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 8)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 7)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 6)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 5)	letouzey