aboutsummaryrefslogtreecommitdiff
path: root/Makefile
AgeCommit message (Collapse)Author
2001-07-16Nettoyagemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1850 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Changement de place et de nom de la tactique Setoid_rewrite.clrenard
Maintenant On appelle Rewrite et il choisit si c'est un setoide ou pas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1838 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la ↵herbelin
compilation native powerpc), le nouveau morceau étant g_ltac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1803 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-20oubli de Elimdep dans le Makefilebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1797 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-12Ajout des entrees puor Setoid_replace.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1783 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-31Creation du fichier Zhints.v repertoriant les thms de ZArith et definissant ↵herbelin
les thms interessants en hints git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1775 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-29Retablissement de minicoqcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1773 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-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-11application patch Claudiofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1746 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-25man pages for coq-interface and parsercourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1717 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-25Ajout pages de man coq_makefile et coqmktopcourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1716 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-25- Ajout pages de man pour coqc, coqtop, coqtop.opt et coqtop.bytecourant
- Deplacement pages de tools/ vers man/ - Modif distrib/Makefile pour Debian - Modif mode emacs pour Debian git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1710 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Ajout de Rseries et Rtrigo_funmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1686 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24suffixes $(EXE) pour bin/parser; quelques binaires oubliés dans make cleanfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1681 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24bin/coqtop est un lien vers bin/coqtop.$(BEST)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1680 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23Ajouts Realsmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1675 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-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-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 Bool/BoolEq.vmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1629 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-19Remplacement Euclid_def Euclid_proof par Euclidmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1617 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19-boot n'implique plus -batchfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1613 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19*** empty log message ***courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1612 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Ajout de Fielddelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1609 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19make sure the binaries needed for the graphical interface will also bebertot
installed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1605 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-18there was a wrong order in the previous version. One was trying tobertot
compile a .vo file before the *.coq files were created. Maybe a missing dependency. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1603 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-18Make sure the binaries needed for pcoq are compiled by default.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1602 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-18Erreur Makefile JMeqmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1601 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-18Adding files for the production of textual explanations as used in pcoq.bertot
dependence files are updated accordingly. Modifications in other files to cope with a few errors in the translation for the parser (mostly around records, coercions, and the search-pattern command). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1599 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-12Ajout de l'egalite de John Majormohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1580 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-10-I contrib/extraction pour compiler Extraction.vfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1574 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-10réparation Correctness; options Extraction (changement de syntaxe)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1571 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-09branchement extraction en standard (pas de Require)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1561 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-08Ajout lemmes arithmetiquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1557 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-05mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1551 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug ↵filliatr
d'ocamldep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1547 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04adding the directives to compile the parser that is used in the graphicalbertot
interface git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1544 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-04add the compilation of the files needed for the interface with pcoq.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1535 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-03installation des .cmo pour l'extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1518 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30branchement extraction (bytecode seulement)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1509 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-29fichiers extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1499 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-28amelioration de la structure des universbarras
elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12Commentaires. Verification des assert false. Probleme des types ML arity.letouzey
Correction des dependances pour bin/coq-extraction dans le Makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1448 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-06modifs pour extraction; bug coqmktopfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1428 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-05module Explore générique et réécriture EAuto avec ce module; occur check ↵filliatr
dans clenv_merge git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1425 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01Inversion termast/astterm; suppression camldebug pour coqmktop -optherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1418 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01nouvelle implantation de la reductionbarras
suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-07 17:27:00 +0000