coq - The formal proof system

Age	Commit message (Expand)	Author
2012-07-29	Fixing #2836 (materialize_evar might refine as a side effect the	herbelin
2012-07-25	Fix eta contraction in Reductionops	pboutill
2012-07-20	Reductionops refactoring	pboutill
2012-07-20	Fixing test-suite	pboutill
2012-07-12	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-11	Fix regression introduced in r15418 that broke MathClasses. In program mode, ...	msozeau
2012-07-10	Another correction to the dependent existential variable printing	aspiwack
2012-07-06	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-06-28	Cleaning opening of the standard List module.	ppedrot
2012-06-25	Added a .mli to pretyping/program.ml	ppedrot
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-21	Fix bug #2791 by doing a fixpoint computation in consider_remaining_problems:	msozeau
2012-06-20	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-15	Reductionops abstract machine uses Zcase & Zfix stack node.	pboutill
2012-06-15	Reductionops : Better abstract machine stack utilities	pboutill
2012-06-04	Replacing some str with strbrk	ppedrot
2012-06-04	Forward-port fixes from 8.4 (15358, 15353, 15333).	msozeau
2012-06-01	More cleaning	ppedrot
2012-06-01	Cleaning Pp.ppnl use	ppedrot
2012-05-30	More uniformisation in Pp.warn functions.	ppedrot
2012-05-29	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-11	Impossible branches inference fixup (bug 2761)	pboutill
2012-04-27	Partial revert of r15148 in order to compile with Camlp4	pboutill
2012-04-25	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-18	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-16	Fixing a "Not_Found" bug related to commit 15061 on the use of evar candidates.	herbelin
2012-04-05	Speedup free_vars_and_rels_up_alias_expansion (evarconv)	gareuselesinge
2012-03-26	Unification: Fixing bug in materialize_evar (spotted by MathClasses).	herbelin
2012-03-26	Unification: Added a heuristic to solve problems of the form	herbelin
2012-03-23	Little bug in r15061 leading to unusable debug mode.	herbelin
2012-03-22	Univ: enforce_leq instead of enforce_geq for more uniformity	letouzey
2012-03-22	evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structures	gareuselesinge
2012-03-20	Fix interface of resolve_typeclasses: onlyargs -> with_goals:	msozeau
2012-03-20	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin