coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Fix bug 2958: Inductive deep in in clause are impossible	pboutill	2013-01-21
*	Last test-suite not in Symmetric Patterns syntax	pboutill	2013-01-21
*	I forget to use git log before git svn dcommit ...	pboutill	2013-01-18
*	Evarconv: Check stack before term in Canonical Structure approuval	pboutill	2013-01-18
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Revert "coq_makefile: use coqdep instead of ocamldep on .ml4 files"	pboutill	2013-01-18
*	Envar: in w32, add .exe when searching for caml binaries	letouzey	2013-01-12
*	Coqmktop and camlp4 : sequel to commit 16113	letouzey	2013-01-12
*	Coq_makefile: quoting paths	pboutill	2013-01-07
*	Coq_makefile: -extra & -phony-extra for user defined makefile rule	pboutill	2013-01-07
*	Fixup notation printing in patterns	pboutill	2013-01-07
*	* Kernel/Terms:	regisgia	2013-01-06
*	Avoiding collision between Camlp4 Loc.Exc_located and Coq's Loc.Exc_located.	herbelin	2012-12-22
*	nat_iter n f x -> nat_rect _ x (fun _ => f) n	pboutill	2012-12-21
*	Yet a new reduction tactic in Coq : cbn	pboutill	2012-12-21
*	Awful heuristic to refold mutual fixpoint in reductionops	pboutill	2012-12-21
*	Fixup and comment reductionops	pboutill	2012-12-21