coq - The formal proof system

Age	Commit message (Expand)	Author
2012-04-23	remove undocumented and scarcely-used tactic auto decomp	letouzey
2012-04-18	Two dead functions in Tacmach.	aspiwack
2012-03-30	Added a command "Unfocused" which returns an error when the proof is	aspiwack
2012-03-30	info_trivial, info_auto, info_eauto, and debug (trivial\|auto)	letouzey
2012-03-30	Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconcl	letouzey
2012-03-23	A unified backtrack mechanism, with a basic "Show Script" as side-effect	letouzey
2012-03-23	Remove old proof-managment commands Suspend/Resume	letouzey
2012-03-21	Pfedit: avoid Undoing too much	letouzey
2012-03-20	Fix interface of resolve_typeclasses: onlyargs -> with_goals:	msozeau
2012-03-20	Arranged for the desirable behaviour that bullets do not see beyond braces.	aspiwack
2012-03-20	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin
2012-03-14	Revise API of understand_ltac to be parameterized by a flag for resolution of...	msozeau
2012-03-14	Integrated obligations/eterm and program well-founded fixpoint building to to...	msozeau
2012-03-14	Second step of integration of Program:	msozeau
2012-03-14	Remove support for "abstract typing constraints" that requires unicity of sol...	msozeau
2012-03-02	Noise for nothing	pboutill
2012-03-01	Corrects the erroneous error message when trying to unfocus a fully	aspiwack
2012-03-01	Removed a superfluous function in proof.mli. Preparing for incoming	aspiwack
2012-02-07	Additional comment on Focus Conditions.	aspiwack
2012-02-07	A "Grab Existential Variables" to transform the unresolved evars at the end o...	aspiwack
2012-02-07	Typo in comments.	aspiwack
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