coq - The formal proof system

Age	Commit message (Expand)	Author
2012-12-18	Fixed a little inefficiency of "set/destruct" over a pattern. Now	herbelin
2012-12-14	Modulification of identifier	ppedrot
2012-12-14	Moved Intset and Intmap to Int namespace.	ppedrot
2012-12-13	Using library string functions.	ppedrot
2012-11-25	Monomorphization (tactics)	ppedrot
2012-11-13	Added a CString module.	ppedrot
2012-11-08	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-18	More cleaning in CArray...	ppedrot
2012-09-18	Cleaning interface of Util.	ppedrot
2012-09-17	More cleaning on Utils and CList. Some parts of the code being	ppedrot
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-09-14	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia
2012-08-08	Updating headers.	herbelin
2012-07-20	Reductionops refactoring	pboutill
2012-07-09	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey
2012-07-05	ZArith + other : favor the use of modern names instead of compat notations	letouzey
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-01	Let's try to avoid generating induction principles for records (wish #2693)	letouzey
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	slim down a bit genarg.ml (pr_intro_pattern forgotten there)	letouzey
2012-05-29	Glob_term now mli-only, operations now in Glob_ops	letouzey
2012-05-29	Tacexpr as a mli-only, the few functions there are now in Tacops	letouzey
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
2012-04-15	In "intro until" and its applications, be consistent when reduction is	herbelin
2012-03-02	Noise for nothing	pboutill
2012-02-20	Use a heuristic to not simplify equality hypotheses remaining after dependent...	msozeau
2012-01-30	Added an pattern / occurence syntax for vm_compute.	ppedrot
2011-12-17	Added a flag to control the use of typing when instantiating applied	herbelin
2011-12-14	Some extra universe refreshing seems needed in abstract_generalize	herbelin
2011-12-12	Proof using ...	gareuselesinge
2011-11-24	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot
2011-11-06	Fixing tactic remember not correctly checking preservation of typing	herbelin
2011-10-22	Use full conversion for checking type of holes in destruct over a	herbelin
2011-10-11	Moved to a more standard order of arguments (i.e. env followed by evar_map)	herbelin
2011-10-05	When a pattern match, don't use the first matching term but an	herbelin
2011-09-26	Added support for referring to subterms of the goal by pattern.	herbelin
2011-09-26	Generalizing subst_term_occ so that it supports an arbitrary matching	herbelin
2011-09-26	Adding subst_term up to conv	herbelin
2011-08-22	Tactics.compute_scheme_signature: factorize the two almost-similar cases	letouzey
2011-08-10	Propagated information from the reduction tactics to the kernel so	herbelin
2011-08-10	Exported tactic intro_then	herbelin
2011-07-29	Tactics: replace generic = on constr by destructors	puech
2011-07-29	Tactics: generic equality on constr replaced by eq_constr	puech
2011-07-29	Tactics: generic equality on constr replaced by eq_constr	puech
2011-07-29	Tactics: generic equality on constr replaced by eq_constr	puech
2011-07-29	Tactics: generic equality on named_declaration replaced by eq_named_declaration	puech
2011-07-16	Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...	herbelin