coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Better implementation for stores.	ppedrot	2013-11-16
*	bugfix micromega: solved an ambiguous symbol resolution	fbesson	2013-11-15
*	Revert "Fast lookup_named in environments, based on maps instead of lists."	ppedrot	2013-11-15
*	Changes the semantics of Ltac's non-lazy pattern matching in presence of mult...	aspiwack	2013-11-14
*	Implementation of Ltac's match and match goal fully based on IStream.	aspiwack	2013-11-14
*	Update comments in matching.mli.	aspiwack	2013-11-14
*	Remove some dead code in tacinterp.	aspiwack	2013-11-14
*	Fast lookup_named in environments, based on maps instead of lists.	ppedrot	2013-11-13
*	Adding an unsafe mapping function to maps.	ppedrot	2013-11-13
*	Synchronizing the printer of tactic notations.	ppedrot	2013-11-13
*	Useless computation in Goal handle augmentation.	ppedrot	2013-11-12
*	Do not print tactic notation names at each interpretation step.	ppedrot	2013-11-12
*	Centralizing the Ltac-defining functions in Tacenv.	ppedrot	2013-11-10
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-10
*	Revert the previous commit. It broke Coq compilation.	ppedrot	2013-11-09
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-09
*	Moving notation types into grammar rule.	ppedrot	2013-11-09
*	Cleaning and documenting Egramcoq.	ppedrot	2013-11-09
*	Partial applications in Goal.	ppedrot	2013-11-09
*	Porting Tactics.assumption to the new engine.	ppedrot	2013-11-08
*	Reverting the old LIFO behaviour of the notation finding algorithm.	ppedrot	2013-11-08
*	Removing partial applications in Reductionops.	ppedrot	2013-11-08
*	Useless array manipulation in Rtrees.	ppedrot	2013-11-08
*	Do not compute formatter UTF8 length at creation time.	ppedrot	2013-11-08
*	Rewriting the proof monad mechanism. Now it uses pure OCaml code, without	ppedrot	2013-11-07
*	Partial application hunt.	ppedrot	2013-11-07
*	Partial application in Globnames.	ppedrot	2013-11-06
*	Less partial applications in Vars, as well as better memory allocation.	ppedrot	2013-11-06
*	better IStream.concat	ppedrot	2013-11-06
*	Preventing useless allocations in Reductionops.instance.	ppedrot	2013-11-05
*	Reducing allocation in tclDISPATCHGEN, by doing a List.map at the same time	ppedrot	2013-11-05
*	STM: fix for PG and "Proof term" lines.	gareuselesinge	2013-11-05
*	Nicer infered names in refine.	aspiwack	2013-11-04
*	Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was sol...	aspiwack	2013-11-04
*	Fix ltac's progress tactical: requires progress in each goal.	aspiwack	2013-11-04
*	Fix the tactical ; [ … ] : the "incorrect number of goal" error was not cau...	aspiwack	2013-11-04
*	Fix change: nf_evar prior to tactic interpretation.	aspiwack	2013-11-04
*	Allowing proofs starting with a non-empty evarmap.	ppedrot	2013-11-04
*	Using allocation-free version of Array higher-order function in critical	ppedrot	2013-11-04
*	Adding closure-preventing functions in CArray. These functions are all	ppedrot	2013-11-04
*	Allocation friendly version of Util.iterate.	ppedrot	2013-11-04
*	Added an update function in CMap. It has the same signature as Map.add, but	ppedrot	2013-11-04
*	Manual coding of Int.Map.find. We use unsafe features, but this function	ppedrot	2013-11-04
*	Evar module now uses default Int maps and sets.	ppedrot	2013-11-04
*	empty token in terminal is a user error not an anomaly (bug 3118)	pboutill	2013-11-03
*	test-suite fixup	pboutill	2013-11-03
*	Asks camlp5 binary in path its location	pboutill	2013-11-03
*	Fixup bug 3145	pboutill	2013-11-03
*	configure stript allows make v4.00	pboutill	2013-11-03
*	Fixing CAMLP4 compilation.	ppedrot	2013-11-02