coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	- Allow parsing of @const@{instance} for specifying universe instances of pol...	Matthieu Sozeau	2014-06-04
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Removing a fishy use of pervasive equality in Ltac backtrace printing.	Pierre-Marie Pédrot	2014-03-01
*	Algebraized "No such hypothesis" errors	Pierre-Marie Pédrot	2014-01-06
*	Do not print tactic notation names at each interpretation step.	ppedrot	2013-11-12
*	Moving potentially costly computation from exception raising to message	ppedrot	2013-10-22
*	Removing uses of Evar.add in class-related functions.	ppedrot	2013-10-06
*	Removing dubious use of evarmap manipulating functions in printing	ppedrot	2013-10-05
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Himsg : strict 80-column indentation	letouzey	2013-08-20
*	Safe_typing code refactoring	letouzey	2013-08-20
*	Added more flags choice in desambiguating printer. The code is	ppedrot	2013-08-06
*	Tentative fix for bug #2961. When we have to print two terms that	ppedrot	2013-08-05
*	Fixing #2846: Uncaught exception Reduction.NotArity.	ppedrot	2013-08-04
*	Using the whole tactic environment while Pretyping.	ppedrot	2013-06-24
*	Generalizing the use of maps instead of lists in the interpretation	ppedrot	2013-06-22
*	Replacing lists by maps in matching interpretation.	ppedrot	2013-06-05
*	Improvement of r16204 on reporting tactic error locations: if the main	herbelin	2013-05-05
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Improving error message in explain_cannot_find_well_typed_abstraction:	herbelin	2013-04-17
*	Fix for bug #3017: wrong handling of the unresolvability status	msozeau	2013-04-03
*	Robust display of NotConvertibleTypeField errors (fix #3008, #2995)	letouzey	2013-03-21
*	Add type information in error message when a constructor is not fully	herbelin	2013-03-21
*	Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical	letouzey	2013-03-14
*	Restrict (try...with...) to avoid catching critical exn (part 13)	letouzey	2013-03-13
*	More monomorphization.	ppedrot	2013-03-05
*	Repairing r16205: errors raised by check_evar_instance were no longer	herbelin	2013-02-28
*	More informative error when a global reference is used in a context of	herbelin	2013-02-28
*	Fixing bug #2466	ppedrot	2013-02-24
*	use List.rev_map whenever possible	letouzey	2013-02-18
*	Displaying environment and unfolding aliases in "cannot_unify"	herbelin	2013-02-17
*	A more informative message when the elimination predicate for	herbelin	2013-02-17
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
*	Revised the Ltac trace mechanism so that trace breaking due to	herbelin	2013-02-17
*	Moved code from Pretype_error to Evarutil	ppedrot	2013-02-10
*	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin	2013-01-29
*	Modulification of Label	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (toplevel)	ppedrot	2012-11-26
*	Added a CString module.	ppedrot	2012-11-13
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box	letouzey	2012-10-06
*	Improving error message when abtraction over goal (abstract_list_all	herbelin	2012-10-04
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Fix typeclass error handling which was sometimes raising a Failure ("hd").	msozeau	2012-07-11