coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adding scrollbars to CoqIDE autocompletion	ppedrot	2013-02-20
*	New autocompletion mechanism in CoqIDE. Now provides many answers	ppedrot	2013-02-19
*	avoid (Int.equal (cmp ...) 0) when a boolean equality exists	letouzey	2013-02-19
*	Dir_path --> DirPath	letouzey	2013-02-19
*	module_path --> ModPath.t, kernel_name --> KerName.t	letouzey	2013-02-19
*	Mod_subst: an extra assert	letouzey	2013-02-19
*	Classops : avoid some use of Gmap	letouzey	2013-02-19
*	Names: revised representation of constants and mutual_inductive	letouzey	2013-02-19
*	Mod_subst: improve sharing during kn substitutions	letouzey	2013-02-18
*	Removing Exc_located and using the new exception enrichement	ppedrot	2013-02-18
*	Adding more primitives to Exninfo	ppedrot	2013-02-18
*	Updating the backtrace handling mechanism to accomodate the new	ppedrot	2013-02-18
*	Added exception enrichment. Now one can define additional arbitrary	ppedrot	2013-02-18
*	use List.rev_map whenever possible	letouzey	2013-02-18
*	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey	2013-02-18
*	Extraction: same as commit 16203, hopefully without NotASort exns	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
*	Locating errors from consider_remaining_unif_problems if possible	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
*	Fix extraction of inductive types that Coq auto-detects to be in Prop	letouzey	2013-02-14
*	CoqIDE: Adding escape reaction to replace widget	ppedrot	2013-02-13
*	Fixing autocompletion lock in CoqIDE	ppedrot	2013-02-13
*	make validate repaired via a temporary fix for #2949	letouzey	2013-02-13
*	Checker: re-sync vo structures after Maxime's commit 16136	letouzey	2013-02-12
*	Fixing bug in native compiler with let patterns in fixpoint definitions.	mdenes	2013-02-11
*	Useless use of hooks in VernacDefinition. In addition, this was	ppedrot	2013-02-10
*	Splitted Evarutil in two files	ppedrot	2013-02-10
*	Moved code from Pretype_error to Evarutil	ppedrot	2013-02-10
*	Revert "Ordered evars by level of dependency in the merging phase of unificat...	herbelin	2013-02-05
*	Fixed bug #2981 (anomaly NotASort in Retyping due to collision between	herbelin	2013-02-05
*	Fixing coqchk compilation after commit r16183	ppedrot	2013-02-03
*	v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)	herbelin	2013-02-01
*	Fixed #2970 (made that remember's eqn name is interpretable as an ltac var).	herbelin	2013-01-29
*	Added a file for testing regression of bug #2955 (anomaly in simpl in	herbelin	2013-01-29
*	No reason a priori for using unfiltered env for printing	herbelin	2013-01-29
*	Fixing bug #2969 (admit failing after Grab Existential Variables due	herbelin	2013-01-29
*	Fixed synchronicity of filter with evar context in new_goal_with.	herbelin	2013-01-29
*	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin	2013-01-29
*	Fixed bug #2966 (de Bruijn error in computation of heads for coercions).	herbelin	2013-01-28
*	Actually adding backtrace handling.	ppedrot	2013-01-28
*	Added backtrace primitives.	ppedrot	2013-01-28
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Fixing one part of #2830 (anomaly "defined twice" due to nested calls to	herbelin	2013-01-28
*	native_compute: Fixed dependencies compilation order.	mdenes	2013-01-28
*	Added backtrace information to anomalies	ppedrot	2013-01-28
*	Ordered evars by level of dependency in the merging phase of unification	herbelin	2013-01-27
*	Improving formatting of output of "Test table".	herbelin	2013-01-27
*	Fixed bug #2967 (some missing check on ill-formed recursive notation strings).	herbelin	2013-01-27