coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...	pboutill	2013-02-25
*	A more informative message when the elimination predicate for	herbelin	2013-02-17
*	Locating errors from consider_remaining_unif_problems if possible	herbelin	2013-02-17
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
*	Splitted Evarutil in two files	ppedrot	2013-02-10
*	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin	2013-01-29
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	- Fix evarconv so that we have complete eta-conversion:	msozeau	2013-01-22
*	Evarconv: Check stack before term in Canonical Structure approuval	pboutill	2013-01-18
*	Reductionops reduction machine can refold constant	pboutill	2012-12-19
*	Evarconv.Pseudorigid erasure	pboutill	2012-12-19
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Evarconv: Fix #2936 + comments	pboutill	2012-11-28
*	Monomorphization (pretyping)	ppedrot	2012-11-22
*	Cleaning and small optimization in CList.	ppedrot	2012-11-20
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	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