coq - The formal proof system

Age	Commit message (Expand)	Author
2013-11-02	Adds a new goal selector "all:".	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	The tactic [admit] exits with the "unsafe" status.	aspiwack
2013-11-02	Cleanup of comments.	aspiwack
2013-11-02	Small change to the IO monad interface: [val ref : 'a -> 'a ref t]	aspiwack
2013-11-02	A whole new implemenation of the refine tactic.	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-10-31	Future: better doc + restore ~pure optimization	gareuselesinge
2013-10-31	Conv_orable made functional and part of pre_env	gareuselesinge
2013-10-29	Do not generate useless argument arrays in whd_* functions.	ppedrot
2013-10-28	Useless array to list conversions in proof/logic.ml.	ppedrot
2013-10-27	Abstracting evar filter away. The API is not perfect, but better than nothing.	ppedrot
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-23	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey
2013-10-23	cList: set-as-list functions are now with an explicit comparison	letouzey
2013-10-18	proof modes: use ephemerons to represent them in proof state	gareuselesinge
2013-10-18	declaration_hooks use Ephemeron	gareuselesinge
2013-10-18	Future: ported to Ephemeron + exception enhancing	gareuselesinge
2013-10-05	Removing dubious use of evarmap manipulating functions in printing	ppedrot
2013-10-05	Moving side effects into evar_map. There was no reason to keep another	ppedrot
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-09-25	Removing useless evar-related stuff.	ppedrot
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-09-18	Removing almost all new_untyped_evar, and a bunch of Evd.add.	ppedrot
2013-09-03	Partly replacing list-based access functions in Evd. This is still	ppedrot
2013-08-30	safe Conv_oracle state for type checking	gareuselesinge
2013-08-25	Replacing lists by sets in clear tactic.	ppedrot
2013-08-08	stm: (initial) support for -coq-slaves	gareuselesinge
2013-08-08	get rid of closures in global/proof state	gareuselesinge
2013-08-08	enhance marshallable option for freeze (minor TODO in safe_typing)	gareuselesinge
2013-08-08	State Transaction Machine	gareuselesinge
2013-06-22	Generalizing the use of maps instead of lists in the interpretation	ppedrot
2013-06-21	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot
2013-06-06	Fixing bug #3030.	ppedrot
2013-06-04	Backtrack on unneeded change of interface for pose_metas_as_evars.	msozeau
2013-06-04	Start documenting new [rewrite_strat] tactic that applies rewriting	msozeau
2013-05-30	Removing a useless location in ltac trace mechanism.	ppedrot
2013-05-28	Getting rid of LtacLocated exception transformer.	ppedrot
2013-05-12	Use the Hook module here and there.	ppedrot
2013-05-09	A uniformization step around understand_* and interp_* functions.	herbelin
2013-05-06	Fixing ocamldoc compilation.	ppedrot
2013-05-03	Removing a redundant function from Evd.	ppedrot
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot