coq - The formal proof system

Age	Commit message (Expand)	Author
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-05-30	Do not compute fallback eagerly in Evarconv	pboutill
2013-05-09	A uniformization step around understand_* and interp_* functions.	herbelin
2013-05-06	Small cleaning of Evd interface.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-04-17	Fix of r16257 in r16205 for "errors raised by check_evar_instance were	herbelin
2013-04-17	Like in r16346, do not filter local definitions (here in the	herbelin
2013-03-30	Continuation of r16346 on filtering local definitions. Refined	herbelin
2013-03-25	Fix bug #2989: make unification.ml able to deal with canonical structure in a...	pboutill
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey
2013-03-05	More monomorphization.	ppedrot
2013-02-28	compare_stack_shape before ise_stack2 in evar_conv	pboutill
2013-02-28	Repairing r16205: errors raised by check_evar_instance were no longer	herbelin
2013-02-25	Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...	pboutill
2013-02-17	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-10	Splitted Evarutil in two files	ppedrot
2013-01-29	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2013-01-22	- Fix evarconv so that we have complete eta-conversion:	msozeau
2013-01-18	Evarconv: Check stack before term in Canonical Structure approuval	pboutill
2012-12-19	Reductionops reduction machine can refold constant	pboutill
2012-12-19	Evarconv.Pseudorigid erasure	pboutill
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