coq - The formal proof system

Age	Commit message (Expand)	Author
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2007-02-07	Correction bug #1364 (les variables de section sont repérées par	herbelin
2006-10-09	Notations:	herbelin
2006-10-06	Annulation de l'essai de changement de sémantique du %scope (révision 9208).	herbelin
2006-10-05	Essai de changement de sémantique du %scope :	herbelin
2006-09-24	Tentative d'amélioration du message d'erreur en cas de paramètre non laissé	herbelin
2006-09-24	Correction bug dans détection clause "in" mal formée quand le "in" est	herbelin
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-09-01	Export de fonctions d'interprétation acceptant des evars non résolues	herbelin
2006-07-03	Extension des motifs disjonctifs au cas de disjonction de motifs multiples	herbelin
2006-06-22	Added {measure x f} as a valid recursion order.	msozeau
2006-06-08	Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...	notin
2006-05-24	Adaptation de Coqdoc au nouveau add_glob	notin
2006-05-23	Retour version 8852 de constrintern.ml	herbelin
2006-05-23	Erreur commit constrintern.ml	herbelin
2006-05-23	Changement de prÃ©cÃ©dence de l'argument du by de assert; consÃ©quences...	herbelin
2006-05-23	Modification de add_glob (support des modules dans Coqdoc)	notin
2006-04-28	r8931@thot: notin \| 2006-04-28 16:19:38 +0200	notin
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-27	préparation de add_glob en vue d'isolement de la partie module pour	herbelin
2006-04-14	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey
2006-03-22	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau
2006-03-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau
2006-03-04	Correction message d'erreur ltac et adoption du modèle de message de Tacinterp	herbelin
2006-01-30	Déplacement du test du bon nombre d'argument des constructeurs (et de	herbelin
2006-01-30	Nettoyage warning (dont flush et affichage seulement si mode verbose)	herbelin
2006-01-09	Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement...	herbelin
2006-01-08	Enregistrement dans glob.dump des utilisations de notations numériques (qui ...	herbelin
2005-12-30	Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-12-22	Correction bugs commit précédent	herbelin
2005-12-21	Restructuration des points d'entrée de Pretyping et Constrintern	herbelin
2005-12-02	Changement des named_context	gregoire
2005-11-19	Correction de la correction du test sur le nombre de parametres d'une projection	herbelin
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-11-02	Types inductifs parametriques	mohring
2005-09-09	Conséquences nettoyage pretyping.ml	herbelin
2005-05-20	Adoption du nom canonique global_of_constr pour éviter confusion avec type r...	herbelin
2005-02-18	Standardisation of function names about global references (especially, renami...	herbelin
2005-01-02	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin
2004-12-24	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin
2004-11-17	Suppression capture des variables par lieurs non liés dans Notation	herbelin
2004-09-15	hiding the meta_map in evar_defs	barras
2004-09-09	Ajout de or-pattern pour le match-with v8	herbelin
2004-08-23	Correction bug #830 : les noms des implicites temporaires étaient inconnus a...	herbelin
2004-08-06	Apply implicit types to local binders too	herbelin
2004-07-16	Abstraction vis à vis du type loc pour compatibilité ocaml 3.08	herbelin
2004-07-16	Nouvelle en-tête	herbelin