coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Goptions do not rely anymore on generic equality.	Pierre-Marie Pédrot	2014-03-03
*	Fixing bad comparison in Detyping.	Pierre-Marie Pédrot	2014-03-01
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	Typo resulting in bad eta-expansion of destructing let's body.	Hugo Herbelin	2013-11-25
*	cList.index is now cList.index_f, same for index0	letouzey	2013-10-23
*	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
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
*	Restrict (try...with...) to avoid catching critical exn (part 7)	letouzey	2013-03-13
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Improving formatting of output of "Test table".	herbelin	2013-01-27
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Modulification of name	ppedrot	2012-12-18
*	Do not display REVERTcast inserted by reduction tactics (unless printing all).	herbelin	2012-12-17
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (pretyping)	ppedrot	2012-11-22
*	More cleaning on Utils and CList. Some parts of the code being	ppedrot	2012-09-17
*	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
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Avoid Pp.std_ppcmds in Misctypes.sort_info	letouzey	2012-08-07
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Replacing some str with strbrk	ppedrot	2012-06-04
*	More uniformisation in Pp.warn functions.	ppedrot	2012-05-30
*	No more Univ in grammar.cma	letouzey	2012-05-29
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin	2012-03-20
*	Glob_term.predicate_pattern: No number of parameters with letins.	pboutill	2012-03-02
*	Noise for nothing	pboutill	2012-03-02
*	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot	2011-11-24
*	Allow "\|_=>_" in "match" in patterns, no more forced enumeration of constructors	letouzey	2011-11-07
*	Remove dynamic stuff from constr_expr and glob_constr	glondu	2011-10-28
*	This is exactly the structure needed to handle controlling printing	herbelin	2011-07-16
*	Fixing bug in printing let-in binders in fix/cofix	herbelin	2011-04-24
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Fixing bug #2279 (printing nested let-in was in exponential time)	herbelin	2010-03-27
*	fixed confusion between number of cstr arguments and number of pattern variab...	barras	2010-03-12
*	In "simpl c" and "change c with d", c can be a pattern.	herbelin	2009-12-24