coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	More Proofview.Goal.enter.	aspiwack	2013-11-02
*	Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).	aspiwack	2013-11-02
*	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack	2013-11-02
*	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	add "Print Ring" and "Print Field" vernacular commands	gareuselesinge	2013-08-30
*	Fixing the code of field_simplify_eq.	amahboub	2013-08-30
*	Added a more efficient way to recover the domain of a map.	ppedrot	2013-08-25
*	Fixing an incompleteness of the ring/field tactics	amahboub	2013-08-23
*	Correcting misplaced Proof command.	amahboub	2013-08-22
*	Fixing a significant efficiency leak in the code of the field tactic.	amahboub	2013-08-22
*	Field_theory : faster and nicer proofs + nice notations.	letouzey	2013-08-22
*	Ring_polynom : shorter proof for Psub_ok	letouzey	2013-08-22
*	Vernac classification streamlined (handles VERNAC EXTEND)	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Expurgating the useless difference between List0 and List1 at the	ppedrot	2013-07-05
*	Now, idtac closures use maps instead of association list.	ppedrot	2013-06-22
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21
*	Hiding tactic value representations.	ppedrot	2013-06-10
*	Uniformizing generic argument types.	ppedrot	2013-06-06
*	newring.ml4: interp constr arg at interp time (not parse time)	gareuselesinge	2013-05-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	code simplifications concerning Summary	letouzey	2013-04-22
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
*	Allowing different types of, not to be mixed, generic Stores through	ppedrot	2013-03-12
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey	2013-02-18
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Modulification of Label	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Stringset and Stringmap to String namespace.	ppedrot	2012-12-14
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey	2012-10-16
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Getting rid of the undocumented [complete] tactic, which was	ppedrot	2012-07-19
*	Ring_polynom : a restricted simpl instead of a unfold;fold	letouzey	2012-07-07
*	Legacy Ring and Legacy Field migrated to contribs	letouzey	2012-07-05
*	rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite	letouzey	2012-07-05
*	More cleanup in Ring_polynom and EnvRing	letouzey	2012-07-05
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05