coq - The formal proof system

Age	Commit message (Expand)	Author
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
2004-04-17	pb facto des Fixpoint + erreur avec -dump-glob et Load	barras
2004-04-08	Chgt role 2eme argument AList et implantation affichage motifs recursifs de n...	herbelin
2004-04-06	Bug sur commit 1.44 dans find_constructor (Not_Found pas rattrape)	herbelin
2004-03-27	Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...	herbelin
2004-03-17	Motifs recursifs de notations: prise en compte de l'associativite et des nota...	herbelin
2004-03-17	Mise en place de motifs récursifs dans Notation; quelques simplifications au...	herbelin
2004-03-12	bug des points fixes (pb avec la contrib Matrices)	barras
2004-03-12	Correction d'un defaut dans la globalisation des variables de notations	herbelin
2004-03-05	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras
2004-02-28	Prise en compte des implicites au travers des notations et abbreviations	herbelin
2004-02-26	Keep structure information for Fixpoint declaration and Fix terms	bertot
2004-02-18	- fixed the Assert_failure error in kernel/modops	barras
2004-02-12	Localisation erreur interp_notation	herbelin
2004-02-12	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin
2004-01-26	reparation de qqs bugs du traducteur	barras
2004-01-22	Correction lecture des locations si pas demandees dans l'ordre	herbelin
2004-01-21	Export information des references de notations pour coqdoc	herbelin
2003-12-19	Substitution dans REvar et PEvar plutot que encodage via noeud application po...	herbelin
2003-11-24	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin
2003-11-19	Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans...	herbelin
2003-11-18	reparation bug moins unaire (erreur de PP)	barras
2003-11-17	Un ident filtre est liant seulement si une variable deja liee (sinon bug dans...	herbelin
2003-11-13	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras
2003-11-01	Extensibilite de la grammaires des patterns	herbelin
2003-10-30	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin
2003-10-14	Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles entre...	herbelin
2003-10-08	Pb residuel avec la prise en compte des parametres implicites d'inductifs	herbelin
2003-10-08	Prise en compte des paramètres implicites d'inductifs pour la globalisation ...	herbelin
2003-09-29	Prise en compte d'un inductif sans argument dans le 'in' des 'match'	herbelin
2003-09-26	Syntaxe plus liberale pour le type des arguments de filtrage du 'match'	herbelin
2003-09-21	Mise en place d'implicites par noms en v8	herbelin