coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added a flag to restrict conversion in tactic unification on the	herbelin	2011-06-13
*	Added a new flag for freezing evars in tactic unification. Used this	herbelin	2011-06-12
*	Moved allow_K to a unification flag	herbelin	2011-06-10
*	Catch AbstractionOverMeta as a unification failure in precatchable_exception.	msozeau	2011-06-07
*	Break circular dependency Proof_global -> Vernacexpr -> Proof_global.	aspiwack	2011-05-17
*	Fixes bug in [maximal_unfocus] introduced in r14120.	aspiwack	2011-05-17
*	A better procedure for checking presence of undefined evars.	aspiwack	2011-05-13
*	The modules in proofs now use the Errors module to explain their exceptions t...	aspiwack	2011-05-13
*	New option [Set Bullet Behavior] allows to select the behaviour of bullets.	aspiwack	2011-05-13
*	First phase removing obsolete support for eta up to conversion in	herbelin	2011-05-04
*	Fixed a bug causing inconsistent states during proof editting.	aspiwack	2011-04-29
*	Some comments.	aspiwack	2011-04-29
*	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau	2011-04-18
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Applying Tom Prince's patch for build_constant_by_tactic not able to	herbelin	2011-04-08
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds	letouzey	2011-03-18
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Forgot a use of evars_reset_evd in nf_evars, add an optional argument as	msozeau	2011-03-10
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	Try to fix the behavior of clenv_missing used when declaring hints	letouzey	2011-02-22
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	Started to fix the declarative proof mode (C-zar).	aspiwack	2011-02-10
*	Factorize code of rewrite to make way for a new implementation using the	msozeau	2011-02-07
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Clenv.connect_clenv without its Evd.fold	letouzey	2010-12-15
*	Goal: preventively replace an Evd.fold by an equivalent Evd.fold_undefined	letouzey	2010-12-13
*	Attempt to preserve casts during a refine, especially VMcast	letouzey	2010-12-10
*	Delayed the evar normalization in error messages to the last minute	herbelin	2010-11-07
*	Fix minor typo in error message (Closes: #2408)	glondu	2010-10-25
*	Remove open_subgoals field of proof_tree	glondu	2010-10-06
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Added eta-expansion in kernel, type inference and tactic unification,	herbelin	2010-09-20
*	In the computation of missing arguments for apply, accept that the	herbelin	2010-09-17
*	Fix [clenv_missing] to compute a better approximation of missing	msozeau	2010-08-02
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proof	herbelin	2010-07-21
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Quick fix for having clenv debug printer working in trunk.	herbelin	2010-06-18
*	Fixed bug #2314 (inversion using not checking the correctness of its arguments	herbelin	2010-06-13
*	Fix bug #2317: setoid_rewrite ignored binding lists. Slightly	msozeau	2010-06-09
*	Automatic introduction of names given before ":" in Lemma's and	herbelin	2010-06-09
*	Fix comment	glondu	2010-06-07
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-06
*	Typo in comment of proof.ml	herbelin	2010-05-29