coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey
2009-03-17	Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)	herbelin
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2009-03-14	Makefile: ml dependencies of contribs are moved to .mllib files	letouzey
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-06	pushed evar reduction in kernel	barras
2009-01-19	Les records déclarés avec Record ne peuvent plus être récursifs (le	aspiwack
2009-01-17	DISCLAIMER	puech
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-12-18	Désactivation de dumpglob lors des appels a functional induction (erreurs pa...	notin
2008-12-14	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau
2008-12-09	About "apply in":	herbelin
2008-11-24	amelioration mineur du comportement de Function	jforest
2008-11-23	first attempt to allow Function to deal with dependent pattern matching. This...	jforest
2008-11-22	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin
2008-11-20	correction of bug #2002	jforest
2008-11-09	More factorization of inductive/record and typeclasses: move class	msozeau
2008-11-05	Move Record desugaring to constrintern and add ability to use notations	msozeau
2008-11-05	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack
2008-10-26	Fixes and refinements regarding occurrence selection:	herbelin
2008-10-26	adding an option Function_raw_tcc to Function	jforest
2008-10-23	Open notation for declaring record instances.	msozeau
2008-10-23	Generalized implementation of generalization.	msozeau
2008-09-12	Add a type argument to letin_tac instead of using casts and recomputing	msozeau
2008-09-11	Add enough information to correctly globalize recursive calls in inductive and	msozeau
2008-08-22	- New auto hints for transparency/opacity control, not bound to	msozeau
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-18	Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...	notin
2008-06-27	Enhanced discrimination nets implementation, which can now work with	msozeau
2008-06-21	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin
2008-06-10	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin
2008-06-08	- Extension de "generalize" en "generalize c as id at occs".	herbelin
2008-06-02	Minor bug correction in recdef	jforest
2008-05-30	Improvements on coqdoc by adding more information into .glob	msozeau
2008-05-06	Postpone the search for the recursive argument index from the user given	msozeau
2008-04-28	menage dans funind + deplaceemnt de recdef dans funind	jforest
2008-04-25	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin
2008-04-24	Remplacement de l'appel à interp_constr pour globaliser une constante	herbelin
2008-04-21	- Parameterize unification by two sets of transparent_state, one for open	msozeau
2008-04-12	Désactivation du dumping des notations quand funind appelle les	herbelin
2008-04-12	Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.	msozeau
2008-04-08	correction of bug 1829	jforest
2008-03-28	- Second pass on implementation of let pattern. Parse "let ' par [as x]?	msozeau
2008-03-18	Added a function to rebuild an elim scheme from elim_scheme_info. Will	courtieu
2008-03-15	Adapt funind to the RLetPattern constructor.	msozeau
2008-03-14	Backtrack wrong commit.	courtieu
2008-03-14	indentation.	courtieu
2008-03-13	trying f	courtieu