coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Slightly improving some debugging printing and error message for modules.	herbelin	2013-01-27
*	Avoid failure in debugger when printing Ltac names.	herbelin	2013-01-27
*	updating ide/coq documentation	ppedrot	2013-01-26
*	Monadification of coqtop queries in CoqIDE	ppedrot	2013-01-26
*	Uniformization of Coq tasks	ppedrot	2013-01-26
*	Better handling of escape find in CoqIDE	ppedrot	2013-01-25
*	Better Undo/Redo mechanism	ppedrot	2013-01-25
*	Trying to fix CoqIDE undo/redo mechanism	ppedrot	2013-01-25
*	Fixing autocompletion in CoqIDE	ppedrot	2013-01-25
*	Fixup last commit	ppedrot	2013-01-25
*	Hugo request: CoqIDE find on enter	ppedrot	2013-01-25
*	Reductionops: whd_state_gen can take and answers a cst_stack too	pboutill	2013-01-24
*	Fixed parsing of -no-native-compiler flag.	mdenes	2013-01-24
*	Native compiler: warnings were not turned off for OCaml 3.11	mdenes	2013-01-24
*	Coqide: limit read buffer size to 4096 (pipe size in win32)	letouzey	2013-01-23
*	Coqide: avoid potentially blocking read on coqtop channel	letouzey	2013-01-22
*	Added .native to .gitignore	ppedrot	2013-01-22
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Revert "remove -rectypes except for term.ml"	mdenes	2013-01-22
*	- Fix evarconv so that we have complete eta-conversion:	msozeau	2013-01-22