aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-04-09mise � jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8175 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-09mise � jour V7; biblio Correctnessfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8174 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-09Mise a jour du chapitre librarymohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8173 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-08Revision Tauto, AutoRewrite + Ajout de Ltacdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8172 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-06mise a jour V7filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8171 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-06debug majletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8170 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-06mise a jour V7filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8169 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-06mise � jour V7filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8168 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-06mise a jour V7filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8167 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-06V7mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8166 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-06Mise a jour V7mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8165 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-06Mise en conformite avec la V7mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8164 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-05ajout chapitre langage de tactiques; suppression chapitre obsoletesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8163 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-03mise a jour V7 de la commande Extraction, et des options de coqtop et coqcfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8162 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-17Les projets de syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8161 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-27Am�liorationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8160 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8159 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Langage de tactiques, AutoRewrite, Tauto-Intuition + autres modifsdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8158 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22MAJ apr�s lecture par Christine; r��criture de la section 'Names'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8157 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22Correctionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8156 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8155 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-21Version lisibleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8154 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18MAJ Searchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8153 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16Ajout \qualid et \moduleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8152 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16RefMan-oth.tex subit d�sormais coq-texherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8151 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16Ajout SearchPattern, SearchRewrite, MAJ Searchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8150 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16Nouveau nom de l'ancien Changes.texherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8149 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15diversfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8148 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15un Reset Initial dans Tutorial.texfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8147 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15config avec autoconffilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8146 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12fichier proposition syntaxefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8145 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12Initial revisionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8143 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-06Création d'un nouveau répertoire docnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8141 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-06Deplacement du répertoire doc dans devnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8140 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-05majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8138 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-05MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8137 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-05Modularisation des preuves concernant la logique classique, ↵herbelin
l'indiscernabilité des preuves et l'axiome K git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8136 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-05Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8135 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-05Exploitation du 'let rec' + présentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8134 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-05New files for subtaccoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8133 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-05Renommage du IP classique pour éviter confusion avec IP constructifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8132 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-05Ajout étude IP généralisé, Gödel-Dummett, buveurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8131 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-05Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une ↵herbelin
référence explicitement de ltac + suppression de la répétition de l'entrée 'reference' dans tactic_atom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8129 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-05Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une ↵herbelin
référence explicitement de ltac + nettoyage unrec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8128 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-05Ajout test relatif au bug #984herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8127 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-04Correction message d'erreur ltac et adoption du modèle de message de Tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8125 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-04majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8124 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-04Petite simplification en passantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8122 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-04Titres moins envahissants pour coqdocherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8121 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-03majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8119 85f007b7-540e-0410-9357-904b9bb8a0f7