coq - The formal proof system

Age	Commit message (Expand)	Author
2007-04-18	- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771	herbelin
2007-02-22	Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme	herbelin
2007-02-21	Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES	herbelin
2006-11-19	Dépendance inutile en Tacexpr, de proofs, qui se compile en principe après	herbelin
2006-11-19	Raffinement de l'unification de "apply": mémorisation de certains	herbelin
2006-10-25	Suite commit 9277	herbelin
2006-10-25	Correction d'une tentative incorrecte (révision 9266) de clarification	herbelin
2006-10-24	Ajout de la tactique "apply in".	herbelin
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-04-07	- Documentation of the Program tactics.	msozeau
2006-03-22	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau
2005-12-02	Changement des named_context	gregoire
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-05-24	Added clenv_environments_evars that behaves as clen_environments but	sacerdot
2004-11-16	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-09-23	error if binder was already defined	barras
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-15	hiding the meta_map in evar_defs	barras
2004-09-12	inclusion de meta_map dans evar_defs	barras
2004-09-10	simplification de clenv	barras
2004-09-08	unification encore...	barras
2004-09-07	deuxieme vague de modifs: evar_defs fonctionnel	barras
2004-09-03	deplacement de clenv vers pretyping	barras