aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-04-23Gros nain avec de Bruijn...letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1668 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23diversfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1667 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23nettoyagefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1666 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23expansion des constr pursfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1665 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23reduction des let in dans whd_programsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1664 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23version 7.0 finalefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1663 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23Uncurryfy_ast inutile depuis l'eta-expansion dans extraction.ml.letouzey
Du coup MLcons avec 2 args seulement. Ne reclame pas de realiser axioms sur Prop. Optimizations=true par default pour Extraction Module. Simplifications naives des letin. Merge_app avant normalisation. Booleen expansion_test pour l'optimisation, avec test de strictness. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1662 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23Remaniement Makefile de test. make reals possibleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1661 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23patch Claudio pour coq_makefilefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1660 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20test Fourier, DiscrRmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1659 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Ajout tactics Realsmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1658 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Ajout Fouriermayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1657 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Ajout Fourier, DiscrR, ...mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1656 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Library doc adjustments (until page 140)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1655 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20optimizations extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1654 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20the file vernacrc, that is necessary to the graphical user-interface pcoqbertot
was not installed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1653 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Mise a la norme lexicalemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1652 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Decomposition de Casesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1651 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Erreurs de Casesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1650 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Retire commenatires obsoletesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1649 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1648 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20un typage sûr pour Goal et Checkfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1647 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Hints.... added next to Hint....coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1646 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Ajout d'erreurs sur le Case avec branche redondantemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1645 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Tests pour Field avec les nombres reelsdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1644 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Ajout de la ligne d'etat pour CVSdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1643 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Petit menagedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1642 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Ajout des entetesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1641 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20support option -R pour coqdepfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1640 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20nettoyagefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1639 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Add a treatement of elaborate Intros tactics, CONJPATTERN and family.bertot
This may not be complete, but it already handles simple cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1638 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Cd est silencieux si -silentfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1637 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19typofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1636 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19scripts; extraction False_recfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1635 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19blindage False_recfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1634 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19cofix; axiomes; eta-expansions pour variables de types mal generalisees (en ↵filliatr
cours) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1633 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Zarith -> ZArithfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1632 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19ajout du cas win32courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1631 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Ajout de fonctions proposees par Cuiht Alvaradomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1630 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Ajout de Bool/BoolEq.vmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1629 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19BoolEq.v, une egalite generique a valeur dans boolmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1628 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19ZArith --> Zarithmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1627 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19synchonization des tables d'extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1626 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19remplace Zarith par ZArithmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1625 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Changement Zarith ZArithmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1624 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19remplace Zarith par ZArithmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1623 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Mise de (*i autour CVS infomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1622 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19modifs des scripts de test autofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1621 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Mise de (*i autour CVS infomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1620 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Mise de (*i autour CVS infomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1619 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 12:21:24 +0000