coq - The formal proof system

Age	Commit message (Expand)	Author
2004-02-12	lazy was translated to cbv, obviously wrong	bertot
2004-02-12	Ajout delimiteur pour bool_scope	herbelin
2004-02-12	MAJ	herbelin
2004-02-12	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin
2004-02-12	Implicits can have an optional list of argument, which is different	bertot
2004-02-12	maj	filliatr
2004-02-11	a new version that uses intro patterns, but the code still needs some cleaning	bertot
2004-02-11	removes a lot comments that may be useful for later code maintenance, but	bertot
2004-02-11	maj	filliatr
2004-02-10	Correction of a bug in Functional Scheme discovered when porting the	coq
2004-02-10	backtrack implicit dans Bvector	marche
2004-02-10	maj	filliatr
2004-02-09	New version of Functional Scheme and functional induction. Deals with	coq
2004-02-09	patch Bvector: args implicites	marche
2004-02-09	maj	filliatr
2004-02-07	maj	filliatr
2004-02-07	maj	filliatr
2004-02-06	MAJ	herbelin
2004-02-06	Test dependencies in constructors	herbelin
2004-02-06	correction de bugs de congruence et firstorder (inductifs)	corbinea
2004-02-06	Ajout filtrage sur motifs dépendants dans des inductifs différents	herbelin
2004-02-06	maj	filliatr
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-05	maj	filliatr
2004-02-05	maj	filliatr
2004-02-04	Reconnaissance précoce de la dépendance du prédicat en un terme filtré	herbelin
2004-02-04	Vérification de la prise en compte des termes de type non inductif	herbelin
2004-02-04	clean-ide plus precis	herbelin
2004-02-04	Localisation un tout petit peu moins abstraite des erreurs de garde, mais res...	herbelin
2004-02-04	Boite autour des quote pour eviter un retour a la ligne apres le premier guil...	herbelin
2004-02-04	bug fix find coqide	coq
2004-02-04	highlight	marche
2004-02-04	search window	coq
2004-02-04	maj	filliatr
2004-02-03	MAJ	herbelin
2004-02-03	Relachement condition pour afficher @ en cas d'explicitation d'implicites	herbelin
2004-02-03	Relachement condition pour declarer un inductif dans la table des 'If'; contr...	herbelin
2004-02-03	Backtrack sur recuperation de noms a partir du type, car casse la correction ...	herbelin
2004-02-03	Bug focus	herbelin
2004-02-03	Protection contre noms de variable indefinis et guillemets autour des constr	herbelin
2004-02-03	Politique de filtrage pour l'affichage plus coercitif pour les lieurs : un no...	herbelin
2004-02-03	maj	filliatr
2004-02-02	reorganize the order of librairies in the entry CMO to make sure this can	bertot
2004-02-02	adds the possibility to mark function arguments as formulas in Ltac	bertot
2004-02-02	adds the possibility to mark function arguments as formulas in Ltac	bertot
2004-01-31	maj	filliatr
2004-01-30	updates the definition of tactics using Ltac and adds the subst tactic	bertot
2004-01-30	adds module commands and update the extration command	bertot
2004-01-30	maj	filliatr