coq - The formal proof system

Age	Commit message (Expand)	Author
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-10-12	- Préservation des appels récursifs de tête dans ltac (réponse au "wish"	herbelin
2007-10-12	Uniformisation du comportement de rewrite et rewrite in : quand le	herbelin
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-09-28	Correction bug 1711	herbelin
2007-06-06	Toujours l'unification de apply : nouveau raffinement pour ne tester	herbelin
2007-05-29	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin
2007-05-28	Contrôle de la compatibilité de apply via une information dans les	herbelin
2007-05-24	Unification suite: petits affinements pour préserver la compatibilité	herbelin
2007-05-23	Tentative d'insertion de coercions avant unification si le type de la	herbelin
2007-05-23	Suite restructuration unification et division des problèmes	herbelin
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2007-05-21	Essai d'une nouvelle heuristique pour clenv_unique_resolver : si le	herbelin
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
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