coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Updating headers.	herbelin	2012-08-08
*	Reductionops refactoring	pboutill	2012-07-20
*	Severe reorganisation of the code of tactics in Proofview.	aspiwack	2012-07-11
*	Small change in the printing of proofs for use by coqide.	aspiwack	2012-07-10
*	Change how the number of open goals is printed.	aspiwack	2012-07-04
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Forward-port fixes from 8.4 (15358, 15353, 15333).	msozeau	2012-06-04
*	Cleaning Pp.ppnl use	ppedrot	2012-06-01
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	Cancel the start of a proof if its init_tac fails (fix #2799)	letouzey	2012-06-01
*	Getting rid of Pp.msg	ppedrot	2012-05-30
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Pattern as a mli-only file, operations in Patternops	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	Tacexpr as a mli-only, the few functions there are now in Tacops	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Pfedit: two superfluous open	letouzey	2012-05-29
*	remove undocumented and scarcely-used tactic auto decomp	letouzey	2012-04-23
*	Two dead functions in Tacmach.	aspiwack	2012-04-18
*	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