coq - The formal proof system

Age	Commit message (Expand)	Author
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-02-15	petits changements cosmetiques sur les tactiques	barras
2002-02-07	petit nettoyage de kernel/inductive	barras
2002-02-01	Ajout tactiques Rename et Pose; modifications pour Inversion	herbelin
2001-12-13	compat ocaml 3.03	filliatr
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-11-05	GROS COMMIT:	barras
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-09-20	Transparent	barras
2001-08-05	Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...	herbelin
2001-07-10	Branchement sur bad_tactic_args	herbelin
2001-03-28	amelioration de la structure des univers	barras
2001-03-15	entetes	filliatr
2001-01-24	Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...	herbelin
2000-12-13	conflit useInversionLemma	mohring
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-12-04	caractere opaque des constantes repris en compte	filliatr
2000-11-06	nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...	filliatr
2000-11-02	correction Abstract (et make world passe!)	filliatr
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-18	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin
2000-10-18	Renommage canonique :	herbelin
2000-09-14	Abstraction de constr	herbelin
2000-09-10	Correction pour make doc	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin
2000-07-01	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-05-22	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin
2000-05-18	Nettoyage	herbelin
2000-05-16	Rien	herbelin
2000-05-05	Intégration de leminv	herbelin
2000-04-30	Intégration progressive	herbelin
2000-03-27	Inversion (pas termine)	filliatr