coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Tacexpr as a mli-only, the few functions there are now in Tacops	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
*	Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml	letouzey	2012-05-29
*	Vernacexpr is now a mli-only file, locality stuff now in locality.ml	letouzey	2012-05-29
*	Fix ocamlbuild compilation: remove subtac from *.itarget	letouzey	2012-04-23
*	correct abort in Function when a proof of inversion fails	letouzey	2012-04-23
*	Corrects a (very) longstanding bug of tactics. As is were, tactic expecting	aspiwack	2012-04-18
*	Remove the Dp plugin.	gmelquio	2012-04-17
*	"A -> B" is a notation for "forall _ : A, B".	pboutill	2012-04-12
*	lib directory is cut in 2 cma.	pboutill	2012-04-12
*	remove plugins/subtac/subtac.ml reintroduced by mistaked in a previous commit	letouzey	2012-04-12
*	info_trivial, info_auto, info_eauto, and debug (trivial\|auto)	letouzey	2012-03-30
*	Module names and constant/inductive names are now in two separate namespaces	letouzey	2012-03-26
*	A unified backtrack mechanism, with a basic "Show Script" as side-effect	letouzey	2012-03-23
*	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin	2012-03-20
*	Fixing bug #2732 (anomaly when using the tolerance for writing	herbelin	2012-03-18
*	Fix merge.	msozeau	2012-03-14
*	Revise API of understand_ltac to be parameterized by a flag for resolution of...	msozeau	2012-03-14
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	Integrated obligations/eterm and program well-founded fixpoint building to to...	msozeau	2012-03-14
*	Everything compiles again.	msozeau	2012-03-14
*	Second step of integration of Program:	msozeau	2012-03-14
*	Remove support for "abstract typing constraints" that requires unicity of sol...	msozeau	2012-03-14
*	Glob_term.predicate_pattern: No number of parameters with letins.	pboutill	2012-03-02
*	Noise for nothing	pboutill	2012-03-02
*	New version of recdef :	jforest	2012-03-01
*	various corrections in invfun due to a modification in induction	jforest	2012-03-01
*	correcting a little bug in invfun.ml	jforest	2012-02-29
*	correction of bug 2457	jforest	2012-02-29
*	In the syntax of pattern matching, "in" clauses are patterns.	pboutill	2012-02-29
*	Correct application of head reduction.	msozeau	2012-02-20
*	Avoid retrying uncessarily to prove independent remaining obligations in Prog...	msozeau	2012-02-15
*	Avoid unnecessary normalizations w.r.t. evars in Program.	msozeau	2012-02-15
*	- Fix dependency computation in eterm to not consider filtered variables.	msozeau	2012-02-14
*	correcting inversion in list of generated tcc of Function	letouzey	2012-02-03
*	Fix camlp4 compilation	pboutill	2012-01-31
*	Added an pattern / occurence syntax for vm_compute.	ppedrot	2012-01-30
*	Fix for Program Instance not separately checking the resolution of evars of t...	msozeau	2012-01-23
*	Another quick hack that works this time, to handle printing of locality in Pr...	ppedrot	2012-01-23
*	Reverted previous commit, which broke library compilation.	ppedrot	2012-01-20
*	This is a quick hack to permit the parsing of the locality flag in the Progra...	ppedrot	2012-01-20
*	Fixed the pretty-printing of the Program plugin.	ppedrot	2012-01-17
*	coq_micromega.ml: fix order of recursive calls to rconstant	glondu	2012-01-14
*	More newlines in debugging output of psatzl	glondu	2012-01-14
*	Added a Btauto plugin, that solves boolean tautologies.	ppedrot	2012-01-13
*	Fix typo	glondu	2012-01-12
*	Moving bullets (-, +, *) into stand-alone commands instead of being	courtieu	2011-12-16
*	Proof using ...	gareuselesinge	2011-12-12
*	Extraction: only do the test on generalizable lets for ocaml	letouzey	2011-12-10