coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added a flag to control the use of typing when instantiating applied	herbelin	2011-12-17
*	Introducing a notion of evar candidates to be used when an evar is	herbelin	2011-12-16
*	Proof using ...	gareuselesinge	2011-12-12
*	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot	2011-11-24
*	In emacs mode, prints a list of the dependent existential variables introduced	aspiwack	2011-11-23
*	Fixing bug #2640 and variants of it (inconsistency between when and	herbelin	2011-11-17
*	Bug 2636 - Move string_of_ppcmds to Pp	pboutill	2011-11-14
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	Applying Tom Prince's patch to support parametric "constructor n" in	herbelin	2011-10-25
*	Moved to a more standard order of arguments (i.e. env followed by evar_map)	herbelin	2011-10-11
*	Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).	herbelin	2011-10-05
*	Moving implicit tactic support from Tacinterp to Pfedit and final evar	herbelin	2011-09-26
*	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack	2011-09-12
*	Remove code concerning the obsolete Set/Unset Undo	letouzey	2011-09-05
*	Porting Hendrik's 8.3 patch for proof tree visualization under proof	herbelin	2011-08-30
*	Remove old file (1999)	msozeau	2011-08-18
*	Fixes mini-bug: Qed would succeed even on focused proofs.	aspiwack	2011-08-12
*	Propagated information from the reduction tactics to the kernel so	herbelin	2011-08-10
*	Fixing typos in comments	herbelin	2011-08-10
*	Graceful error message for [Proof Mode] and [Set Default Proof Mode] when req...	aspiwack	2011-08-10
*	Stores bullet stack on locally at the level of focuses rather than globally i...	aspiwack	2011-07-11
*	Fixed bullets so that they would play well with { }.	aspiwack	2011-07-06
*	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey	2011-07-04
*	Cleaning debugging printer relative to new proof engine. In	herbelin	2011-06-21
*	Generalizing flag use_evars_pattern_unification into a flag	herbelin	2011-06-18
*	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