aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-06Création d'un nouveau répertoire docnotin
2006-03-06Deplacement du répertoire doc dans devnotin
2006-03-05majcoq
2006-03-05MAJherbelin
2006-03-05Modularisation des preuves concernant la logique classique, l'indiscernabilit...herbelin
2006-03-05Commentairesherbelin
2006-03-05Exploitation du 'let rec' + présentationherbelin
2006-03-05New files for subtaccoq
2006-03-05Renommage du IP classique pour éviter confusion avec IP constructifherbelin
2006-03-05Ajout étude IP généralisé, Gödel-Dummett, buveurherbelin
2006-03-05Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf...herbelin
2006-03-05Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf...herbelin
2006-03-05Ajout test relatif au bug #984herbelin
2006-03-04Correction message d'erreur ltac et adoption du modèle de message de Tacinterpherbelin
2006-03-04majcoq
2006-03-04Petite simplification en passantherbelin
2006-03-04Titres moins envahissants pour coqdocherbelin
2006-03-03majcoq
2006-03-02majcoq
2006-03-02Correction bug #1097 (dû à une typo...)herbelin
2006-03-02Ajout test bug 1089herbelin
2006-03-02Correctif pour bug #1089 (cannot define an isevar twice)herbelin
2006-03-02tactic haRVey pour appeler haRVey (contrib/dp)filliatr
2006-03-02Correction du bug 808: il est maintenant interdit de déclarer une assomption...coq
2006-03-01Correction bug #842 (rename d'une hyp du contexte)herbelin
2006-03-01appel de Zenonfilliatr
2006-02-28majcoq
2006-02-28*** empty log message ***filliatr
2006-02-27majcoq
2006-02-27quelques raccourcis commodes + un f_equal plus efficaceletouzey
2006-02-27dp: sortie Whyfilliatr
2006-02-26majcoq
2006-02-25majcoq