coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Minor cleanup concerning Mod_subst.MBImap	letouzey	2013-04-02
*	Exporting the SearchAbout filter.	ppedrot	2013-04-02
*	Continuation of r16346 on filtering local definitions. Refined	herbelin	2013-03-30
*	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-28
*	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-26
*	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-25
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
*	NMake*: avoid some warning about Let outside sections	letouzey	2013-03-22
*	Fix bug# 2994, 2971 about better error messages.	msozeau	2013-03-22
*	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-21
*	Check a list length before doing a List.chop (fix #3000)	letouzey	2013-03-20
*	Better encapsulation of MessageView	ppedrot	2013-03-20
*	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-19
*	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-18
*	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-17
*	another Errors.push in a exception reraise	letouzey	2013-03-16
*	Extract_env : correct exceptions mentionned in a try ... with	letouzey	2013-03-15
*	Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical	letouzey	2013-03-14
*	Cerrors: get rid of some FIXME	letouzey	2013-03-14