coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Nouveau Rewrite-in plus economique	barras	2002-03-04
*	compat ocaml 3.03	filliatr	2001-12-13
*	Diverses petites simplications de la machine de preuves.	clrenard	2001-11-19
*	Suppression des stamps et donc des *_constraints	clrenard	2001-11-12
*	GROS COMMIT:	barras	2001-11-05
*	Incompatibilité entre la prise en compte des univers au niveau des tactiques...	herbelin	2001-10-10
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	amelioration de la structure des univers	barras	2001-03-28
*	entetes	filliatr	2001-03-15
*	print_id, print_sp -> pr_id, pr_sp	herbelin	2000-11-23
*	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
*	C'était pas le bon env dans build_term	herbelin	2000-10-11
*	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin	2000-09-12
*	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
*	Nettoyage de Generic	herbelin	2000-05-31
*	suppression ligne etrange	herbelin	2000-05-18
*	ciseaux	herbelin	2000-05-18
*	Retrait du i pour tclTHEN_i et correction bugs Decompose	herbelin	2000-05-16
*	gros commit de tout ce que j'ai fait pendant les vacances :	filliatr	2000-01-21
*	- environment -> safe_environment	filliatr	1999-12-01
*	typage des existentielles dans Typing_ev; suppression metamap inutiles dans t...	filliatr	1999-11-25
*	module Wcclausenv	filliatr	1999-11-22