coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Avancée vers la prise compte des alias dépendants; prise en compte des clau...	herbelin	2001-03-11
*	Pb génération noms Cases + mise en place mécanisme d'histoire du filtrage ...	herbelin	2001-03-05
*	uniformisation avec constr des lieurs dans rawterm/pattern	herbelin	2001-02-14
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
*	Bug prédicat	herbelin	2000-12-25
*	Amélioration message d'erreur mauvais prédicat	herbelin	2000-12-18
*	Suppression du warning several default clauses	herbelin	2000-12-16
*	Bugs calcul du prédicat des Cases et Case	herbelin	2000-12-15
*	Mauvais env donné à new_isevar	herbelin	2000-12-14
*	Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases devien...	herbelin	2000-12-14
*	Bug Cases en presence d'une absence de clause	herbelin	2000-12-05
*	Utilisation de global_reference dans rawconstr	herbelin	2000-11-20
*	suppression des (* open Generic *)	filliatr	2000-11-02
*	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin	2000-10-18
*	Renommage canonique :	herbelin	2000-10-18
*	Renommage des find_m*type	herbelin	2000-10-11
*	Prise en compte de Let dans build_dependent_inductive	herbelin	2000-10-11
*	Correction de bugs (alias initiaux et ordre des cas par défaut)	herbelin	2000-10-10
*	Correction incompatibilites dans la fn des types des inductifs	herbelin	2000-10-06
*	Renommage AppL en App; Suppression cast	herbelin	2000-10-01
*	Abstraction de constr	herbelin	2000-09-14
*	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin	2000-09-12
*	Correction pour make doc	herbelin	2000-09-10
*	Suppression de Abst	herbelin	2000-09-10
*	Ajout d'un LetIn primitif.	herbelin	2000-09-10
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
*	Plus de env et sigma dans get_arity, plus de sigma dans make_arity	herbelin	2000-07-01
*	Extension de find_inductive aux co-inductifs et renommage en find_rectype	herbelin	2000-07-01
*	Extension de l'inférence des types des lambdas du prédicat	herbelin	2000-06-29
*	Bugs	herbelin	2000-06-09
*	bugs infrence des arguments manquants dans le prdicat	herbelin	2000-06-02
*	Bugs et simplifications coercions	herbelin	2000-06-02
*	Mise en place d'un choix constr/typed_type en remplacement de certains Cast	herbelin	2000-06-01
*	Nettoyage de Generic	herbelin	2000-05-31
*	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin	2000-05-22
*	Effets de bords suite à la restructuration des inductives (cf Inductive)	herbelin	2000-05-18
*	Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)	herbelin	2000-05-04
*	pattern-matching non-exhaustif (occur_rawconstr)	filliatr	2000-05-02
*	Retrait fullmind de inductive_summary pour simplicité	herbelin	2000-04-27
*	Introduction d'un type constr_pattern pour les différents filtrages	herbelin	2000-04-26
*	Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...	herbelin	2000-03-21
*	Qqes bugs (evars dans le predicat; tag des cas défauts)	herbelin	2000-03-16
*	Reparation bug isevars dans pretyping	herbelin	2000-03-10
*	Un nouveau moteur pour Cases (phase 1)	herbelin	2000-03-08
*	Abstraction de l'implémentation des signatures de Sign en vue intégration d...	herbelin	2000-01-26
*	Correction pbs liés aux evar	herbelin	2000-01-07
*	Bug lift	herbelin	1999-12-15
*	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin	1999-12-15
*	Poursuite intégration du Cases	herbelin	1999-12-13
*	Intégration initiale du Cases	herbelin	1999-12-11