coq - The formal proof system

Age	Commit message (Expand)	Author
2009-04-08	- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing	herbelin
2009-04-03	Fix obvious bug in evars_of_named_context.	msozeau
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2009-03-28	Fix bug #2056 (discharge bug).	msozeau
2009-03-22	Compromise wrt introduction-names compatibility issue after addition	herbelin
2009-03-20	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey
2009-03-20	Fixes to make Ynot compile with the trunk:	msozeau
2009-03-04	Backtrack sur la mémoïsation de nf_evar.	aspiwack
2009-02-27	=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...	aspiwack
2009-02-20	On passe les last_mods (un des champs de Evd.evar_defs) de list	aspiwack
2009-02-20	On ne met plus rien dans les last_mods tant que conv_pbs est vide.	aspiwack
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2009-02-09	memoized is_ground_env	barras
2009-02-06	pushed evar reduction in kernel	barras
2009-02-06	From v8.2 to trunk:	herbelin
2009-01-23	Really compare evar maps in progress, due to merging in apply and other	msozeau
2009-01-20	Fixing bug #1918 (no occur-check in Meta unification was done yet!).	herbelin
2009-01-20	- Fixing bug 1891 (abusive instantiations of evar arguments in	herbelin
2009-01-18	Backporting from v8.2 to trunk:	herbelin
2009-01-17	DISCLAIMER	puech
2009-01-16	Correct a bug in commit 11659	puech
2009-01-12	Fix a bunch of bugs related to setoid_rewrite, unification and evars:	msozeau
2009-01-05	Completed 11745 (move of jprover to user contribs) and cleaned 11743	herbelin
2009-01-04	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin
2009-01-02	Fixed two apparent inconsistencies in matching.ml:	herbelin
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-12-26	- Extracted from the tactic "now" an experimental tactic "easy" for small	herbelin
2008-12-06	Fix exponential behaviour of the typeclasses persistent objects. Drop	puech
2008-12-04	Fixes for unification and substitution of metas under binders.	msozeau
2008-12-03	improved simpl	barras
2008-12-02	Miscellaneous fixes and improvements:	herbelin
2008-11-28	another bug with simpl	barras
2008-11-27	Fix (?) a pattern matching compilation problem:	msozeau
2008-11-27	fixed bug 1791: simpl was performing eta expansion	barras
2008-11-27	fixing problem with CompCert: reordering resulting from tac change was not cl...	barras
2008-11-21	fixed problem with r11612	barras
2008-11-21	fixed exponential behavior of evar unif (ground case)	barras
2008-11-14	Restores behaviour of v8.1 for unification problems which fail (backport of 1...	letouzey
2008-11-09	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin
2008-11-08	Apply vmconv if there are no _undefined_ evars around.	msozeau
2008-11-07	Slight change of the semantics of user-given casts: they don't really	msozeau
2008-11-07	Fix universe problem appearing ConCaT using the existing infrastructure for	msozeau
2008-11-05	Fix in the unification algorithm using evars: unify types of evar	msozeau
2008-11-05	Move Record desugaring to constrintern and add ability to use notations	msozeau
2008-10-26	Fixes and refinements regarding occurrence selection:	herbelin
2008-10-26	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin
2008-10-25	More debugging of handling of open constrs with typeclasses:	msozeau
2008-10-23	Open notation for declaring record instances.	msozeau