aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2001-04-06debug majletouzey
2001-04-06mise a jour V7filliatr
2001-04-06mise � jour V7filliatr
2001-04-06mise a jour V7filliatr
2001-04-06V7mohring
2001-04-06Mise a jour V7mohring
2001-04-06Mise en conformite avec la V7mohring
2001-04-05ajout chapitre langage de tactiques; suppression chapitre obsoletesfilliatr
2001-04-03mise a jour V7 de la commande Extraction, et des options de coqtop et coqcfilliatr
2001-01-17Les projets de syntaxeherbelin
2000-12-27Am�liorationsherbelin
2000-12-26MAJherbelin
2000-12-25Langage de tactiques, AutoRewrite, Tauto-Intuition + autres modifsdelahaye
2000-12-22MAJ apr�s lecture par Christine; r��criture de la section 'Names'herbelin
2000-12-22Correctionsherbelin
2000-12-21MAJherbelin
2000-12-21Version lisibleherbelin
2000-12-18MAJ Searchherbelin
2000-12-16Ajout \qualid et \moduleherbelin
2000-12-16RefMan-oth.tex subit d�sormais coq-texherbelin
2000-12-16Ajout SearchPattern, SearchRewrite, MAJ Searchherbelin
2000-12-16Nouveau nom de l'ancien Changes.texherbelin
2000-12-15diversfilliatr
2000-12-15un Reset Initial dans Tutorial.texfilliatr
2000-12-15config avec autoconffilliatr
2000-12-12fichier proposition syntaxefilliatr
2000-12-12Initial revisionfilliatr
2006-03-06Deplacement du répertoire doc dans devnotin
2005-02-06Nettoyage et documentation de Libraryherbelin
2005-01-21MAJherbelin
2004-03-02Tactic Notation et with-namesherbelin
2004-02-18- fixed the Assert_failure error in kernel/modopsbarras
2004-01-29Suppression de 'Print.' en v8herbelin
2004-01-09bugs avec Pose et Assertbarras
2003-12-24*** empty log message ***barras
2003-12-24*** empty log message ***barras
2003-12-24MAJ Notationherbelin
2003-12-23*** empty log message ***barras
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
2003-12-04MAJ 'abstract'herbelin
2003-11-27Reparation bug compilmohring
2003-11-25modif lexer: ident peut commencer par _barras
2003-11-23MAJsherbelin
2003-11-13moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...barras
2003-11-13factorisation et generalisation des clausesbarras
2003-11-12petits changements de syntaxebarras
2003-11-09'as' avant 'using' dans 'destruct'herbelin
2003-11-05Oubliherbelin
2003-11-05MAJherbelin
2003-11-05MAJherbelin