coq - the Coq proof assistant

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