aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2005-08-12majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7288 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-11majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7286 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-10majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7284 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-09majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7282 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-08majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7280 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7278 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-06majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7276 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-05majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7274 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-04majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7272 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-03majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7270 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7268 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7267 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7265 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7264 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7262 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-01Procédure d'ajout d'une nouvelle contributions utilisateurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7261 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-25Add two .bat scripts to run coq and coqide under windows without changing ↵narboux
autoexec.bat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7260 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-25rename INSTALL.win INSTALL.txt to ease openingnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7259 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7257 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-23majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7255 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-22majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7253 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-21majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7251 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-21Utilisation de la non-équivalence d'inductifs pour le case_info (cf message ↵herbelin
CP et EC dans coqdev) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7250 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-20majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7248 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-18majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7245 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7243 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-16majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7241 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-15majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7239 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-15majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7238 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-15Subtac: traitement correct des existentielles et de la récursion.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7237 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-15Add some debug printing functions.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7236 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-15Fix sumbool_not hint (on behalf of cpaulin).coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7235 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-15add a left and right tactic for classical logicnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7234 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-15reflexive tautocorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7233 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-15improves shadows in the main windownarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7232 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-15foldherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7231 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-14majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7228 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-14majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7227 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7225 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7224 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13Détection d'un Fold incorrect suite à correction bug #986herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7223 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7220 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13Détection d'un Fold incorrect suite à correction bug #986herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7219 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13General recursive definitions on well founded orders supportcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7217 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13reactivation de l optim des fermeturesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7216 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13backtrack modif de knh...barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7215 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13Correction double bug #986: Fold ne préserve pas nécessairement le typage ↵herbelin
et test de conversion buggé dans Logic.convert_hyp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7212 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-13*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7211 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-12majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7209 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-12test du tag de reductionbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7208 85f007b7-540e-0410-9357-904b9bb8a0f7