coq - The formal proof system

Age	Commit message (Expand)	Author
2016-03-21	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot
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
2002-02-01	Ajout tactiques Rename et Pose; modifications pour Inversion	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-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-29	Ajout du Let pour le langage de tactiques	delahaye
2000-12-18	Renommages autour de NewInduction	herbelin
2000-12-12	Hint Unfold Local + commentaires	mohring
2000-11-26	Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...	herbelin
2000-10-13	Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...	herbelin
2000-07-21	Modifs d'interpretation de patterns	delahaye
1999-11-23	modules Indrec, Tacentries, Hiddentac	filliatr