coq - The formal proof system

Age	Commit message (Expand)	Author
2013-04-15	Checker: get rid of code handling section variables	letouzey
2013-04-15	Checker: empty sections hardcoded in cb and mind	letouzey
2013-04-15	Checker: reified encoding of .vo types in values.ml	letouzey
2013-04-15	Checker: regroup all vo-related types in cic.mli	letouzey
2013-04-15	anew_instance should not consume the locality twice	gareuselesinge
2013-04-15	More functional implementation of locality_flag and program_mode	gareuselesinge
2013-04-11	Backport r16394 from 8.4:	msozeau
2013-04-10	Equality: avoid some unprotected List.nth (fix #2837)	letouzey
2013-04-09	Added a module of immutable arrays. Not as full as CArray, but should	ppedrot
2013-04-08	Enrich test-suite with a test for #3022.	ppedrot
2013-04-05	Allow catching of WrongAbstractionType, fixing a regression from 8.4	msozeau
2013-04-04	Small doc fix : module subtyping cannot force access of opaques	letouzey
2013-04-03	Removing two Pervasives.compare from Term.	ppedrot
2013-04-03	Fix for bug #3017: wrong handling of the unresolvability status	msozeau
2013-04-02	Revised infrastructure for lazy loading of opaque proofs	letouzey
2013-04-02	Mod_subst.force: avoid using join when only one subst	letouzey
2013-04-02	Minor cleanup concerning Mod_subst.MBImap	letouzey
2013-04-02	Exporting the SearchAbout filter.	ppedrot
2013-03-30	Continuation of r16346 on filtering local definitions. Refined	herbelin
2013-03-28	Safe_typing+Libary: use some arrays instead of lists in vo structures	letouzey
2013-03-28	Safe_library : a record type for compiled_library instead of large tuple	letouzey
2013-03-26	Synchronizing loadpath with the backtrack mechanism.	ppedrot
2013-03-26	Moved the Loadpath part of Library to its own file, and documented	ppedrot
2013-03-25	Typo in refman (fix #2962)	letouzey
2013-03-25	Enrich test-suite with a test for #2928	letouzey
2013-03-25	Enrich test-suite with a test for #2734	letouzey
2013-03-25	Native compiler: hash-consing of generated code and values.	mdenes
2013-03-25	Add the test-case of bug 2750 in the test-suite	letouzey
2013-03-25	Native compiler: timing info for reification in debug mode.	mdenes
2013-03-25	Native compiler: Inlined constants are now compiled, fixing a bug reported by	mdenes
2013-03-25	Normalized type for Vector.map2	pboutill
2013-03-25	Fix bug #2989: make unification.ml able to deal with canonical structure in a...	pboutill
2013-03-25	cbn can be called by Eval	pboutill
2013-03-25	Comments in mli	pboutill
2013-03-23	Minor code cleaning in CArray / CList.	ppedrot
2013-03-22	NMake*: avoid some warning about Let outside sections	letouzey
2013-03-22	Fix bug# 2994, 2971 about better error messages.	msozeau
2013-03-21	Fixing unfolding of local definitions during unification that appeared	herbelin
2013-03-21	Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.	herbelin
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