coq - The formal proof system

Age	Commit message (Expand)	Author
2012-12-14	Modulification of identifier	ppedrot
2012-12-14	Moved Intset and Intmap to Int namespace.	ppedrot
2012-11-28	Evarconv: Fix #2936 + comments	pboutill
2012-11-22	Monomorphization (pretyping)	ppedrot
2012-11-20	Cleaning and small optimization in CList.	ppedrot
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-14	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-08-09	Unification in Evar_conv uses an abstract machine state	pboutill
2012-08-08	Updating headers.	herbelin
2012-07-20	Reductionops refactoring	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-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-15	Reductionops : Better abstract machine stack utilities	pboutill
2012-05-29	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-03-26	Unification: Added a heuristic to solve problems of the form	herbelin
2012-03-22	evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structures	gareuselesinge
2012-03-20	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-02	Noise for nothing	pboutill
2011-12-16	Introducing a notion of evar candidates to be used when an evar is	herbelin
2011-12-04	Discarding let-ins from the instances of the evars in the	herbelin
2011-11-08	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-06	Fixing incorrect change to pattern-unification over Meta's introduced	herbelin
2011-10-26	Deactivating second-order pattern-matching in evarconv for 8.4.	herbelin
2011-10-24	Fixing instance/filter mismatch in materialize_evar + documentation.	herbelin
2011-10-22	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-11	Completing r14538 (Chung-Kil Hur's trick for fast dependently-typed	herbelin
2011-10-10	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-07-29	Evarconv: generic equality on constr replaced by eq_constr	puech
2011-06-19	Ensured that the transparency state is used when flag betaiota is on for apply.	herbelin
2011-05-24	Applying Enrico Tassi's patch for giving priority to delta over eta in	herbelin
2011-03-31	As remarked by Enrico, we'd better use eq_constr than structural equality	herbelin
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
2011-03-11	Tentative to make unification check types at every instanciation of an	msozeau
2011-03-07	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