aboutsummaryrefslogtreecommitdiff
path: root/Makefile
AgeCommit message (Collapse)Author
2000-11-20Prise en compte camlp4.opt dans la configuration et le Makefileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@874 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-11Prise en compte camlp4.opt dans la configuration et le Makefileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@844 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09-I states dans les includes de Coqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@833 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09-I theories/Init pour faire initial.coqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@832 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09coqc appele avec -bindir binfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@831 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08nouveau load pathfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@828 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08tous les binaires maintenant dans le repertoire binfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@822 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Modification de la table des tactic Definitions pour eviter l'ecrituremohring
de fonctions dans les .vo ajout de lemmes dans EqNat, Logic_Type suppression de PolyListSyntax qui redefinissait le Infix de append Recherche d'instances a reecrire dans les Cases et les FixPoint git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@820 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des ↵filliatr
constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@807 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-05Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier ↵herbelin
devenu tros gros pour la compilation en PowerPC git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@800 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-03Few OCaml files in contrib/xmlsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@798 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-03compilation avec make de Solaris; README et INSTALLfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@797 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-03compilation des fichiers ml4 sans GNUseriesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@795 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-02suppression des (* open Generic *)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-31- simplification Makefile (compilation des fichiers .ml'; pas encore parfaitfilliatr
car on passe par les fichiers .ml) - Require Export enfin rétabli avec la bonne sémantique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@792 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-30Ajouts pour les tactiques utilisateurdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@783 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27g_natsyntax et g_zsyntax maintenant toujours linkesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@773 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26ntrefiner.ml* removed in module xmlsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@762 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-25xml contribution added to the Makefilesacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@757 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@719 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-18mise a jour dependancesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@613 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Suppression Redinfo Sosub Abstractionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@605 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Ajout d'un LetIn primitif.herbelin
Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-21Pattern -> parsingdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@560 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-20portage Refinefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@559 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-05Adaptation pour Alpha.delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@556 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-05Adaptation pour alpha.delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@555 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Utilisation du STRIP de config/Makefile pour gérer le mode profileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@533 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21portage EAuto et Ringfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@513 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-12dependance des CONTRIBVO envers initial.coqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@504 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-22Changement nom module Constant en Declarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@459 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18Restructuration des outils pour les inductifs.herbelin
- Les déclarations (mutual_inductive_packet et mutual_inductive_body), utilisisées dans Environ vont dans Constant - Instantiations du context local (mind_specif), instantiation des paramètres globaux (inductive_family) et instantiation complète (inductive_type, nouveau nom de inductive_summary) vont dans Inductive qui est déplacé après réduction - Certaines fonctions de Typeops et celle traitant des inductifs dans Reduction et Instantiate sont regroupées dans Inductive" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@444 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05Intégration de leminvherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@422 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-04Vernacinterp passe après Commandherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@418 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03nettoyage (quelques oublis dans make clean)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@414 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03compilation bytecode / native :filliatr
- script de configuration - Makefile - simplification de coqmktop - option -opt de coqc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@413 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03Ajout du langage de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-02portage Omega (mais toujours pas Zpower et Zlogarithm)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@400 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-30MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@392 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@386 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28portage Omega (code seulement)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@381 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28portage en ocaml / camlp4 3.00filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@379 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26Débranchement provisoire equality et tautoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@374 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-21Compilation pbs (coqc not finding coqtop, coqc not finding .vo whencourant
building states, coqc wrongly giving option -bindir to coqtop) fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@365 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21 - bug make_module_marker (plus de # et de .obj maintenant)filliatr
- portage (partiel) de Zarith - bug discrEverywhere (manquait un "fun gls ->") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@353 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-20Tautofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@331 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-18ZArithfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@327 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-18on ne compile pas Div.v (Realizer)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@325 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-16theories/Boolfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@319 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-10Eqdep_dec doit etre compilefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@314 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 10:00:50 +0000