coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Unification in Evar_conv uses an abstract machine state	pboutill	2012-08-09
*	Updating headers.	herbelin	2012-08-08
*	Reductionops refactoring	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
*	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
*	Reductionops : Better abstract machine stack utilities	pboutill	2012-06-15
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	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
*	Unification: Added a heuristic to solve problems of the form	herbelin	2012-03-26
*	evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structures	gareuselesinge	2012-03-22
*	Generalized the use of evar candidates in type inference unification:	herbelin	2012-03-20
*	Reorganizing the structure of evarutil.ml (only restructuration, no	herbelin	2012-03-20
*	Noise for nothing	pboutill	2012-03-02
*	Introducing a notion of evar candidates to be used when an evar is	herbelin	2011-12-16
*	Discarding let-ins from the instances of the evars in the	herbelin	2011-12-04
*	Refined second_order_matching so that a constraint on which	herbelin	2011-11-08
*	optimization: memoization for is_open_canonical_projection	gareuselesinge	2011-11-08
*	Improved check is_open_canonical_projection	gareuselesinge	2011-11-08
*	Fixing incorrect change to pattern-unification over Meta's introduced	herbelin	2011-11-06
*	Deactivating second-order pattern-matching in evarconv for 8.4.	herbelin	2011-10-26
*	Fixing instance/filter mismatch in materialize_evar + documentation.	herbelin	2011-10-24
*	Fail if some conv pbs remain after consider_remaining_unif_problems.	herbelin	2011-10-22
*	Use also second-order unification if first-order fails at the time of conside...	herbelin	2011-10-22
*	Completing r14538 (Chung-Kil Hur's trick for fast dependently-typed	herbelin	2011-10-11
*	More robust and uniform treatment of aliases in evarutil.ml	herbelin	2011-10-10
*	Applied the trick of Chung-Kil Hur to solve second-order matching	herbelin	2011-10-10
*	Evarconv: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Ensured that the transparency state is used when flag betaiota is on for apply.	herbelin	2011-06-19
*	Applying Enrico Tassi's patch for giving priority to delta over eta in	herbelin	2011-05-24
*	As remarked by Enrico, we'd better use eq_constr than structural equality	herbelin	2011-03-31
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Tentative to make unification check types at every instanciation of an	msozeau	2011-03-11
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Revert commit r13883: instantiating ?n by a lambda when "?n a" has to	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	Added support for instantiation of ?n by a lambda when "?n a" has to	herbelin	2011-03-05
*	Reorganized a bit evarconv.ml:	herbelin	2011-03-05
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	Added eta-expansion in kernel, type inference and tactic unification,	herbelin	2010-09-20
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29