coq - The formal proof system

Age	Commit message (Expand)	Author
2012-01-30	Added an pattern / occurence syntax for vm_compute.	ppedrot
2012-01-20	Added documentation for "r foo" in Ltac debugger.	herbelin
2012-01-20	Breakpoints in Ltac debugger: new command "r foo" to jump to the next	herbelin
2012-01-06	Forbids (as it has always been the behaviour) to have two different open	aspiwack
2012-01-06	Fixes bug #2654 (tactic instantiate failing to update existential variables).	aspiwack
2011-12-18	Granted legitimate wish #2607 (not exposing crude fixpoint body of	herbelin
2011-12-17	Added a flag to control the use of typing when instantiating applied	herbelin
2011-12-16	Introducing a notion of evar candidates to be used when an evar is	herbelin
2011-12-12	Proof using ...	gareuselesinge
2011-11-24	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot
2011-11-23	In emacs mode, prints a list of the dependent existential variables introduced	aspiwack
2011-11-17	Fixing bug #2640 and variants of it (inconsistency between when and	herbelin
2011-11-14	Bug 2636 - Move string_of_ppcmds to Pp	pboutill
2011-11-02	Add type annotations around all calls to Libobject.declare_object	letouzey
2011-10-25	Applying Tom Prince's patch to support parametric "constructor n" in	herbelin
2011-10-11	Moved to a more standard order of arguments (i.e. env followed by evar_map)	herbelin
2011-10-05	Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).	herbelin
2011-09-26	Moving implicit tactic support from Tacinterp to Pfedit and final evar	herbelin
2011-09-12	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack
2011-09-05	Remove code concerning the obsolete Set/Unset Undo	letouzey
2011-08-30	Porting Hendrik's 8.3 patch for proof tree visualization under proof	herbelin
2011-08-18	Remove old file (1999)	msozeau
2011-08-12	Fixes mini-bug: Qed would succeed even on focused proofs.	aspiwack
2011-08-10	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-07-11	Stores bullet stack on locally at the level of focuses rather than globally i...	aspiwack
2011-07-06	Fixed bullets so that they would play well with { }.	aspiwack
2011-07-04	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey
2011-06-21	Cleaning debugging printer relative to new proof engine. In	herbelin
2011-06-18	Generalizing flag use_evars_pattern_unification into a flag	herbelin
2011-06-13	Added a flag to restrict conversion in tactic unification on the	herbelin
2011-06-12	Added a new flag for freezing evars in tactic unification. Used this	herbelin
2011-06-10	Moved allow_K to a unification flag	herbelin
2011-06-07	Catch AbstractionOverMeta as a unification failure in precatchable_exception.	msozeau
2011-05-17	Break circular dependency Proof_global -> Vernacexpr -> Proof_global.	aspiwack
2011-05-17	Fixes bug in [maximal_unfocus] introduced in r14120.	aspiwack
2011-05-13	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-04	First phase removing obsolete support for eta up to conversion in	herbelin
2011-04-29	Fixed a bug causing inconsistent states during proof editting.	aspiwack
2011-04-29	Some comments.	aspiwack
2011-04-18	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-04-08	Applying Tom Prince's patch for build_constant_by_tactic not able to	herbelin
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2011-03-18	A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds	letouzey
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau