coq - The formal proof system

Age	Commit message (Expand)	Author
2000-03-07	Export inh_conv_coerce_to et divers	herbelin
2000-03-07	Redondances	herbelin
2000-03-07	Export mis_typed_arity	herbelin
2000-03-07	Ajout destApplication	herbelin
2000-03-07	Nettoyage check_pos	herbelin
2000-03-07	Renommage ppterm0 --> ppterm	herbelin
2000-03-07	Capture des exceptions si env vide pour ne pas echouer lors du debogage	herbelin
2000-03-07	Ajout matrix_transpose	herbelin
2000-01-31	Export gentermpr avec renommage	herbelin
2000-01-31	Force le renommage dans bad_ind_arguments	herbelin
2000-01-28	documentation	filliatr
2000-01-27	erreurs latex dans interfaces	filliatr
2000-01-26	mise a jour	filliatr
2000-01-26	lorsque ocamlc est donne a la main, alors ocamlopt est positionne avec	filliatr
2000-01-26	MAJ ocaml 2.99 (espaces dans la syntaxe des cast)	herbelin
2000-01-26	Fin du changement comarg -> constrarg	herbelin
2000-01-26	MAJ commentaires	herbelin
2000-01-26	Abstraction de l'implémentation des signatures de Sign en vue intégration d...	herbelin
2000-01-21	gros commit de tout ce que j'ai fait pendant les vacances :	filliatr
2000-01-20	Bête renommage	herbelin
2000-01-20	Broutilles	herbelin
2000-01-13	Nettoyage des fichiers de parsing	herbelin
2000-01-13	Plus d'unfold inutile des Fix dans Simpl	herbelin
2000-01-11	Ajout de Record	herbelin
2000-01-11	Bugs	herbelin
2000-01-11	Ajout '\|' en tete de filtrage	herbelin
2000-01-07	Grammaire pour Grammar et Syntax, avant dans Extend	herbelin
2000-01-07	Traduction constr->rawconstr (avant dans Termast	herbelin
2000-01-07	Restructuration printer et parser	herbelin
2000-01-07	Restructuration diverses	herbelin
2000-01-07	MAJ	herbelin
2000-01-07	Renommage command en constr	herbelin
2000-01-07	Déplacement print_emacs dans Options	herbelin
2000-01-07	Correction pbs liés aux evar	herbelin
2000-01-07	Déplacement non-affichage des coercions dans termast	herbelin
2000-01-07	Restructuration printer et parser	herbelin
2000-01-07	Renommage command en constr	herbelin
1999-12-16	erreurs de syntax :$	filliatr
1999-12-16	bug : import -> export dans Require	filliatr
1999-12-15	message erreur Scheme	herbelin
1999-12-15	Bug lift	herbelin
1999-12-15	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin
1999-12-15	Les inductifs dans Scheme doivent être des ident d'inductifs	herbelin
1999-12-14	clarification du code	filliatr
1999-12-14	rattrapage exceptions autres que UserError	filliatr
1999-12-14	sauvegarde de la valeur de module_name	filliatr
1999-12-14	bug mk_clenv_from lorsque pas d arguments	filliatr
1999-12-14	pretty-printers pour le debugger	filliatr
1999-12-13	mise a jour de refiner.ml (reports de modifs de la V6.3)	barras
1999-12-13	- états fabriqués avec -silent	filliatr