aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2001-06-19Un bug corrige.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1796 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-12Ajout de la tactique Setoid_replace.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1782 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-29Facilites pour le debogguage des univers.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1772 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-28Pretty -> Prettypfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1768 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-28patch Claudiofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1766 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-28nettoyagefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1765 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-25Oups: flingait les Dglob dans optimizeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1764 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-22majletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1760 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-22suite du musée des horreursletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1759 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-22ordre des inductifs + axiome-typeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1758 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-18Modification afin de permettre plusieurs modifs successives d'une commandeclrenard
vernac (ici la commande Save) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1756 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-14mise en place extraction haskellfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1751 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-14réparation Ring (simplifications)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1750 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-11application patch Claudiofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1746 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-11bug castletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1745 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-10exemples Magicletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1742 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-10message 'is defined' seulement en mode verbosefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1741 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-10retouche de extract_inductive_declarationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1740 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-09nettoyage extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1737 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-09cleanup + comments, toujoursletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1736 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-07integration de field a fouriermayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1734 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-04commentairesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1732 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-03Changement de la structure des points fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-02commentaires sur renommages des var dans extract_typeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1730 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-30cleanup, commentsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1729 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-30ocamlwebfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1728 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-30commentaires mlutil + binders_fold en coursletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1727 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-25make reals prend en compte tous les .vo de theories/Realsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1712 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Suppression d'une partie de code commentedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1700 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24README avec ref (2)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1695 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24TODO in v.o., test/Makefile moins pire, README avec refletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1694 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Ajout du .dependmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1693 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Retire theories/Nummohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1692 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Correction typosmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1690 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24ajout d'un fichier READMEletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1689 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Fin d'optimisation (cas modules) + warning pour coind & ocamlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1685 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24cofix_warning dans les parametres d'extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1683 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Removing a debug message for the search command.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1678 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23forme codefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1673 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23mise a jourletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1671 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23realisation des realsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1670 85f007b7-540e-0410-9357-904b9bb8a0f7
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-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-20Ajout Fouriermayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1657 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:16:48 +0000