coq - The formal proof system

Age	Commit message (Expand)	Author
2008-05-28	Notation concise pour la valeur par défaut des cas reconnus comme	herbelin
2008-05-05	Mise en place d'un algorithme d'inversion des contraintes de type lors	herbelin
2008-04-01	Finish enhancemenent of return clause inference from tycons, integrating	msozeau
2008-03-29	Fix test-suite files, change conflicting notation "->rel" and the others	msozeau
2008-03-28	- Second pass on implementation of let pattern. Parse "let ' par [as x]?	msozeau
2008-01-17	Add new LetPattern construct to replace dest. syntax: let\| pat := t in b is b...	msozeau
2007-12-31	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-09-25	Suppression de tous les alias de la forme x:=x dans la compilation du filtrage.	herbelin
2007-09-06	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin
2007-08-10	- Correction d'un bug de de Bruijn dans abstract_predicate (lié au	herbelin
2007-03-15	Suppression argument pattern_source du case_info (code jamais utilisé)	herbelin
2006-11-22	Code mort découvert par Matthieu	herbelin
2006-10-05	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin
2006-09-23	Correction d'un bug de coercion de pattern introduit dans la 8.1beta	herbelin
2006-05-29	The "clean integration of subtac" patch.	msozeau
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-04-28	Typo dans précédent commit (8755); protection renforcée dans analyse claus...	herbelin
2006-04-27	- Distinction explicite des parties paramètres et arguments dans le type	herbelin
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-04-25	Code mort (suite)	herbelin
2006-04-25	Suppression code mort	herbelin
2006-04-14	Pas fier	herbelin
2006-04-10	Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...	msozeau
2006-04-07	- Documentation of the Program tactics.	msozeau
2006-03-22	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau
2006-01-30	Suppression fonctions d'interprétation du vieux Case	herbelin
2006-01-30	- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer	herbelin
2006-01-30	- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer;	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-08-19	pas besoin de List.length pour savoir si une liste est vide	letouzey
2005-08-19	Sur le conseil de X.Leroy: x=[\|\|] devient Array.length x=0	letouzey
2005-06-08	evar declarees avec mauvais type	barras
2005-04-29	Fix bug in prepare_predicate_from_tycon; improved error message when no claus...	herbelin
2004-12-09	Correction du bug de build_initial_predicate a révèlé un autre bug dans ex...	herbelin
2004-12-08	Bugs dans la déclaration du type du terme filtré si non défini	herbelin
2004-12-03	Propagation du nom des hyps du prédicat de filtrage pour le message d'erreur...	herbelin
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-15	hiding the meta_map in evar_defs	barras
2004-09-07	deuxieme vague de modifs: evar_defs fonctionnel	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-04-13	Correction confusion entre la dependance en les termes filtrees dans l'annota...	herbelin
2004-03-28	Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...	herbelin
2004-02-27	Erreur de Bruijn et oubli substitution alias dans annotation du 'match'	herbelin
2004-02-05	On s'affranchit de l'information inductif ou pas dans le prédicat (càd	herbelin
2004-02-05	Suppression des types dans la signature du predicat (ils sont	herbelin
2004-02-04	Reconnaissance précoce de la dépendance du prédicat en un terme filtré	herbelin
2003-12-27	Type le 'return' comme un type	herbelin
2003-11-19	Deplacement subst_rawconstr dans Rawterm	herbelin