coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Partial revert of Yann commit in order to use CLib.List when opening	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
*	correct some ends of .mllib files (avoid a broken tolink.ml)	letouzey	2012-08-24
*	Unification in Evar_conv uses an abstract machine state	pboutill	2012-08-09
*	Updating headers.	herbelin	2012-08-08
*	Avoid Pp.std_ppcmds in Misctypes.sort_info	letouzey	2012-08-07
*	Fixing #2836 (materialize_evar might refine as a side effect the	herbelin	2012-07-29
*	Fix eta contraction in Reductionops	pboutill	2012-07-25
*	Reductionops refactoring	pboutill	2012-07-20
*	Fixing test-suite	pboutill	2012-07-20
*	flex_maybeflex factoring	pboutill	2012-07-12
*	miller_pfenning unification code factoring	pboutill	2012-07-12
*	flex_kind_of_term does not have a copy of term	pboutill	2012-07-12
*	evar reduction is already made by whd_*	pboutill	2012-07-12
*	tacred uses stack_reduction_function instead of state_reduction_function	pboutill	2012-07-12
*	Fix regression introduced in r15418 that broke MathClasses. In program mode, ...	msozeau	2012-07-11
*	Another correction to the dependent existential variable printing	aspiwack	2012-07-10
*	Continuing r15459: it helps testing occur-check early in some	herbelin	2012-07-06
*	Practical fix for bug #1206 (anomaly raised in pretyping instead of	herbelin	2012-07-06
*	Fixes bug #2678	aspiwack	2012-07-06
*	Cleaning opening of the standard List module.	ppedrot	2012-06-28
*	Added a .mli to pretyping/program.ml	ppedrot	2012-06-25
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Fix bug #2791 by doing a fixpoint computation in consider_remaining_problems:	msozeau	2012-06-21
*	Fixing use of an error instead of a boolean result in the unification	herbelin	2012-06-20
*	Fixing bug #2817 (occur check was not done up to instantiation of	herbelin	2012-06-20
*	Reductionops abstract machine uses Zcase & Zfix stack node.	pboutill	2012-06-15
*	Reductionops : Better abstract machine stack utilities	pboutill	2012-06-15
*	Replacing some str with strbrk	ppedrot	2012-06-04
*	Forward-port fixes from 8.4 (15358, 15353, 15333).	msozeau	2012-06-04
*	More cleaning	ppedrot	2012-06-01
*	Cleaning Pp.ppnl use	ppedrot	2012-06-01
*	More uniformisation in Pp.warn functions.	ppedrot	2012-05-30
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
*	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
*	Pattern as a mli-only file, operations in Patternops	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	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
*	Impossible branches inference fixup (bug 2761)	pboutill	2012-05-11
*	Partial revert of r15148 in order to compile with Camlp4	pboutill	2012-04-27
*	Avoid unneeded head-normalizations in coercion code.	msozeau	2012-04-25
*	Do not delta-head-normalize the proposition argument of sigma types during co...	msozeau	2012-04-25
*	Corrects a bug in the refine tactic which could drop evar bodies.	aspiwack	2012-04-18
*	Adds a comment: precondition on Evd.add	aspiwack	2012-04-18
*	Fixing a "Not_Found" bug related to commit 15061 on the use of evar candidates.	herbelin	2012-04-16