coq - The formal proof system

Age	Commit message (Expand)	Author
2016-03-20	Moving the Ltac definition command to an EXTEND based command.	Pierre-Marie Pédrot
2016-03-20	Moving the tactic related code from Metasyntax to a new file.	Pierre-Marie Pédrot
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2001-11-19	Diverses petites simplications de la machine de preuves.	clrenard
2001-10-05	Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...	herbelin
2001-09-21	make doc	filliatr
2001-08-07	Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...	herbelin
2001-08-05	Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction	herbelin
2001-03-15	entetes	filliatr
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-07-25	retablissement make doc et make minicoq	filliatr
2000-07-21	Modifs d'interpretation de patterns	delahaye
2000-05-03	Ajout du langage de tactiques	delahaye
1999-11-24	Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations	filliatr
1999-11-23	modules Indrec, Tacentries, Hiddentac	filliatr