aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2005-03-11Ajout de COQLIB/user-contrib à l'installation pour insister sur la possibili...herbelin
2005-03-11Ajout récursif du répertoire COQLIB/user-contrib au chemin de chargementherbelin
2005-03-10majcoq
2005-03-10A défaut de substitution paresseuse ou explicite, ajout d'une substitution o...herbelin
2005-03-10A défaut de substitution paresseuse ou explicite, ajout d'une substitution o...herbelin
2005-03-09majcoq
2005-03-09bug #931 (continued): no recursion on the evars instantiationherbelin
2005-03-08majcoq
2005-03-08majcoq
2005-03-08Fix bug #931: leave dependent evars as such for refineherbelin
2005-03-08Ajout foldherbelin
2005-03-07majcoq
2005-03-07Added 'clear - id' to clear all hypotheses except the ones dependent in the s...herbelin
2005-03-07Added 'clear - id' to clear all hypotheses except the ones dependent in the s...herbelin
2005-03-06majcoq
2005-03-06the package script disappeared in MacOS 10.3: we locally copy the 10.2 versionherbelin
2005-03-05majcoq
2005-03-04majcoq
2005-03-03majcoq
2005-03-02majcoq
2005-03-01majcoq
2005-03-01clean de parser.optherbelin
2005-03-01Code mortherbelin
2005-03-01MAJherbelin
2005-02-28majcoq
2005-02-27majcoq
2005-02-26majcoq
2005-02-25majcoq
2005-02-24majcoq
2005-02-23majcoq
2005-02-23quelques tactics ltacletouzey
2005-02-22majcoq
2005-02-22Suppression des fichiers temporairesherbelin
2005-02-21majcoq
2005-02-21majcoq
2005-02-21*** empty log message ***herbelin
2005-02-21Pas de dépendance en Omegaherbelin
2005-02-21Correction de bugs: coq_false et coq_true au lieu de coq_False et coq_trueherbelin
2005-02-21- changement ordre arguments interp_goal_concl pour permettre applicationherbelin
2005-02-21- Correction de bugsherbelin
2005-02-20majcoq
2005-02-20Keep ClosedSection marker for resetherbelin
2005-02-19majcoq
2005-02-18majcoq
2005-02-18majcoq
2005-02-18Moving subst_inductive from tacinterp to inductiveops for better for reuse in...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_functionherbelin
2005-02-18Renaming Print Canonical Structure into Print Canonical Projectionsherbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin