coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.	ppedrot	2012-06-12
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	Getting rid of Pp.msg	ppedrot	2012-05-30
*	place all files specific to camlp4 syntax extensions in grammar/	letouzey	2012-05-29
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Everything compiles again.	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Proof using ...	gareuselesinge	2011-12-12
*	Fixing bug #2640 and variants of it (inconsistency between when and	herbelin	2011-11-17
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	Esubst: make types of substitutions & lifts private	puech	2011-08-08
*	moins de reification inutile, noatations standards	pottier	2011-08-04
*	Newring: generic = on constr replaced by eq_constr	puech	2011-07-29
*	replaced some generic = on constr by eq_constr	puech	2011-07-29