coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	More Proofview.Goal.enter.	aspiwack	2013-11-02
*	Added the tactical "tac1 + tac2".	aspiwack	2013-11-02
*	Try to remove intermediate allocations when dealing with goal-specific tactics.	aspiwack	2013-11-02
*	Various rewriting, mostly for speed purposes.	aspiwack	2013-11-02
*	Fix behaviour of the refine tactic with respect to evars in types.	aspiwack	2013-11-02
*	Makes the Ltac debugger usable again.	aspiwack	2013-11-02
*	Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...	aspiwack	2013-11-02
*	Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).	aspiwack	2013-11-02
*	Clean up a warning.	aspiwack	2013-11-02
*	The tactic [admit] exits with the "unsafe" status.	aspiwack	2013-11-02
*	Cleanup of comments.	aspiwack	2013-11-02
*	A whole new implemenation of the refine tactic.	aspiwack	2013-11-02
*	A newly introduced variable inside a named context is no longer α-renamed.	aspiwack	2013-11-02
*	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack	2013-11-02
*	Bases tactics on an IO monad.	aspiwack	2013-11-02
*	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack	2013-11-02
*	Uses Proofview.tclEXTEND more sparingly.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Conv_orable made functional and part of pre_env	gareuselesinge	2013-10-31
*	Evar leak in "absurd" tactic.	ppedrot	2013-10-28
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	Tacintern: avoid a match (fst (List.hd ...))	letouzey	2013-10-23
*	declaration_hooks use Ephemeron	gareuselesinge	2013-10-18
*	Removing uses of Evar.add in class-related functions.	ppedrot	2013-10-06
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05
*	Fixing potential evar leak in Rewrite, and removing dead code.	ppedrot	2013-10-05
*	Fixing potential evar leak in Equality.	ppedrot	2013-10-05
*	Splitting Class_tactics between code and CAMLP4/5 declarations.	ppedrot	2013-10-04
*	Made rewrite tactic strategies pure. They were using quite uglily	ppedrot	2013-09-28
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Opacifying the type of strategies.	ppedrot	2013-09-26
*	Splitting Rewrite into a code part and a CAMLP4-dependent one.	ppedrot	2013-09-26
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Removing unused code from Term_dnet.	ppedrot	2013-09-18
*	Optimizing some evar_maps manipulation. In particular, using a [map] instead	ppedrot	2013-09-05
*	Some cleanup in Auto	ppedrot	2013-09-03
*	Removing some lone List.assoc & List.mem in lib.	ppedrot	2013-08-28
*	Actually using the domain function for maps.	ppedrot	2013-08-25
*	Less "Coq" strings everywhere	letouzey	2013-08-22
*	get rid of closures in global/proof state	gareuselesinge	2013-08-08
*	Vernac classification streamlined (handles VERNAC EXTEND)	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Side effect free implementation of admit (Isabelle's oracle)	gareuselesinge	2013-08-08
*	Small fix in IStream interface.	ppedrot	2013-08-08
*	Fixing #3062. Computation of the value of a fresh identifier was	ppedrot	2013-08-04
*	Removing useless casts between arrays and lists.	ppedrot	2013-08-04
*	Small cleaning of printing coercion failures in Ltac interpretation.	ppedrot	2013-08-04
*	Small fixes due to the arrival of OCaml 3.12.	ppedrot	2013-08-03