coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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-30
*	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-23
*	Pfedit: avoid Undoing too much	letouzey	2012-03-21
*	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-20
*	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-14
*	Noise for nothing	pboutill	2012-03-02
*	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-03-01
*	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-02-07
*	Added an pattern / occurence syntax for vm_compute.	ppedrot	2012-01-30
*	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-20
*	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	2012-01-06
*	Granted legitimate wish #2607 (not exposing crude fixpoint body of	herbelin	2011-12-18
*	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