coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Changement des named_context	gregoire	2005-12-02
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Changement dans les boxed values .	gregoire	2004-11-12
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	unification encore...	barras	2004-09-08
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	Unification lemInv et lemInv_in	herbelin	2003-10-10
*	Utilisation du second-ordre avec possibilité de K-rédex dans lemInv	herbelin	2002-12-24
*	suite du commit precedent	barras	2002-12-19
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15
*	petit nettoyage de kernel/inductive	barras	2002-02-07
*	Ajout tactiques Rename et Pose; modifications pour Inversion	herbelin	2002-02-01
*	compat ocaml 3.03	filliatr	2001-12-13
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
*	GROS COMMIT:	barras	2001-11-05
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
*	Transparent	barras	2001-09-20
*	Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...	herbelin	2001-08-05
*	Branchement sur bad_tactic_args	herbelin	2001-07-10
*	amelioration de la structure des univers	barras	2001-03-28
*	entetes	filliatr	2001-03-15
*	Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...	herbelin	2001-01-24
*	conflit useInversionLemma	mohring	2000-12-13
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	caractere opaque des constantes repris en compte	filliatr	2000-12-04
*	nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...	filliatr	2000-11-06
*	correction Abstract (et make world passe!)	filliatr	2000-11-02
*	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
*	Abstraction de constr	herbelin	2000-09-14
*	Correction pour make doc	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