coq - The formal proof system

Age	Commit message (Expand)	Author
2000-05-16	Rien	herbelin
2000-05-05	Achèvement nettoyage Pfedit; ajout intros_replacing	herbelin
2000-05-05	Intégration de leminv	herbelin
2000-05-04	les erreurs	herbelin
2000-05-04	Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)	herbelin
2000-05-04	Nettoyage de l'interface de Pfedit	herbelin
2000-05-03	Reparation du bug d'interpretation d'Abstract	delahaye
2000-05-03	diverses modifs pour ocamlweb	filliatr
2000-05-03	MAJ	herbelin
2000-05-03	Ajout get_reference	herbelin
2000-05-03	Encapsulage de PatternMatchingFailure par un 'error' pour que l'echec de conc...	herbelin
2000-05-03	Ajout du langage de tactiques	delahaye
2000-05-02	Divers	herbelin
2000-05-02	Problème avec motif du second-ordre	herbelin
2000-04-30	Suite intégration de constr_pattern	herbelin
2000-04-30	Intégration progressive	herbelin
2000-04-30	Adaptés pour le type constr_pattern et les nouvelles fonctions de filtrage	herbelin
2000-04-28	Déplacement du type reference dans Term	herbelin
2000-04-28	Déplacement du type reference dans Term	herbelin
2000-04-28	Decoupage de tactics/pattern en proofs/pattern et tactics/hipattern	herbelin
2000-04-28	Changement de représentation du contexte des réf dans rawconstr et pattern	herbelin
2000-04-26	Introduction d'un type constr_pattern pour les différents filtrages	herbelin
2000-04-26	Nettoyage	herbelin
2000-04-20	Abstraction du type typed_type (un pas vers les jugements 2 niveaux)	herbelin
2000-03-30	erreurs lexicales dans les patterns (manquait des espaces)	filliatr
2000-03-28	Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf...	herbelin
2000-03-27	Inversion (pas termine)	filliatr
2000-03-21	- bug make_module_marker (plus de # et de .obj maintenant)	filliatr
2000-03-21	Modification de type_of_case, type_case_branches, etc;nettoyage	herbelin
2000-03-21	MAJ ocaml 2.99	herbelin
2000-03-21	Prise en compte nouveau case_info et nouvel Reduction.instance	herbelin
2000-03-20	Tauto	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	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-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-13	- états fabriqués avec -silent	filliatr
1999-12-13	- méthode load sur les Hints	filliatr
1999-12-13	documentation	filliatr
1999-12-07	debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkes	filliatr
1999-12-05	premier debugage	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-01	poursuite de Vernacentries	filliatr
1999-12-01	- environment -> safe_environment	filliatr
1999-12-01	- Typing -> Safe_typing	filliatr