coq - The formal proof system

Age	Commit message (Expand)	Author
2000-05-22	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin
2000-05-18	bug (typage avec meta)	herbelin
2000-05-18	Effets de bords suite à la restructuration des inductives (cf Inductive)	herbelin
2000-05-18	doc	herbelin
2000-05-16	Retrait du i pour tclTHEN_i et correction bugs Decompose	herbelin
2000-05-05	Achèvement nettoyage Pfedit	herbelin
2000-05-04	Nettoyage de l'interface de Pfedit	herbelin
2000-05-03	compilation bytecode / native :	filliatr
2000-05-03	Completion d'un match non exhaustif	delahaye
2000-05-03	diverses modifs pour ocamlweb	filliatr
2000-05-03	Ajout du langage de tactiques	delahaye
2000-05-02	portage Omega (mais toujours pas Zpower et Zlogarithm)	filliatr
2000-05-02	Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'	herbelin
2000-04-30	Suite intégration de constr_pattern	herbelin
2000-04-28	Renommage bdize -> ast_of_constr	herbelin
2000-04-28	Decoupage de tactics/pattern en proofs/pattern et tactics/hipattern	herbelin
2000-04-28	chgt unify_0	herbelin
2000-04-26	Introduction d'un type constr_pattern pour les différents filtrages	herbelin
2000-04-20	Abstraction du type typed_type (un pas vers les jugements 2 niveaux)	herbelin
2000-03-28	Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf...	herbelin
2000-03-21	Modification de type_of_case, type_case_branches, etc	herbelin
2000-03-21	Remplacement plain_instance en instance qui n'a plus besoin de env	herbelin
2000-03-17	Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'	herbelin
2000-01-28	documentation	filliatr
2000-01-26	MAJ ocaml 2.99 (espaces dans la syntaxe des cast)	herbelin
2000-01-26	Abstraction de l'implémentation des signatures de Sign en vue intégration d...	herbelin
2000-01-07	Renommage command en constr	herbelin
1999-12-15	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin
1999-12-14	rattrapage exceptions autres que UserError	filliatr
1999-12-14	bug mk_clenv_from lorsque pas d arguments	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
1999-12-13	- méthode load sur les Hints	filliatr
1999-12-10	- erreurs Pretype	filliatr
1999-12-10	debug reset	filliatr
1999-12-09	- constantes avec recettes	filliatr
1999-12-08	deplacement de Discharge dans toplevel	filliatr
1999-12-07	debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkes	filliatr
1999-12-05	premier debugage	filliatr
1999-12-03	- coqmktop	filliatr
1999-12-03	modules profile, Coqinit et Coqtop (=main)	filliatr
1999-12-03	- global_reference traite des variables	filliatr
1999-12-02	modifs pour premiere edition de liens	filliatr
1999-12-02	Pfedit (fin)	filliatr
1999-12-01	poursuite de Vernacentries	filliatr
1999-12-01	module Pfedit	filliatr
1999-12-01	- environment -> safe_environment	filliatr
1999-12-01	- Typing -> Safe_typing	filliatr
1999-11-29	portage modules Evarconv et Evarutil	filliatr
1999-11-25	typage des existentielles dans Typing_ev; suppression metamap inutiles dans t...	filliatr