aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
Commit message (Collapse)AuthorAge
* Commit fixes from v8.2 branch (r11386 and r11387)Gravatar glondu2008-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11390 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalize usage of $(FIND_VCS_CLAUSE) and add debian to itGravatar glondu2008-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11389 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not install csdpcert in $(BINDIR)Gravatar glondu2008-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11388 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleaningGravatar glondu2008-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11370 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use $(COQTOPEXE) to refer to bin/coqtop in MakefilesGravatar glondu2008-09-06
| | | | | | | | The environment variable COQTOP has a different meaning for Coq executables and for Coq Makefiles, which is troublesome when make forwards it to subprocesses via the environment. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11366 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renaming parser -> coq-parserGravatar glondu2008-08-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11328 85f007b7-540e-0410-9357-904b9bb8a0f7
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Correction divers messages d'erreur - lorsque rien à réécrire dans une hyp, - lorsqu'une variable ltac n'est pas liée, - correction anomalie en présence de ?id dans le "as" de induction, - correction mauvais env dans message d'erreur de unify_0. - Diverses extensions et améliorations - "specialize" : - extension au cas (fun x1 ... xn => H u1 ... un), - renommage au même endroit. - "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize". - "induction" - intro des IH toujours au sommet même si induction sur var quantifiée, - ajout d'un hack pour la reconnaissance de schémas inductifs comme N_ind_double mais il reste du boulot pour reconnaître (et/ou réordonner) les composantes d'un schéma dont les hypothèses ne sont pas dans l'ordre standard, - vérification de longueur et éventuelle complétion des intropatterns dans le cas de sous-patterns destructifs dans induction (par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas le n dans le contexte), - localisation des erreurs d'intropattern, - ajout d'un pattern optionnel après "as" pour forcer une égalité et la nommer (*). - "apply" accepte plusieurs arguments séparés par des virgules (*). - Plus de robustesse pour clear en présence d'evars. - Amélioration affichage TacFun dans Print Ltac. - Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu (incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !). - Fusion VTactic/VFun dans l'espoir. - Mise en place d'un système de trace de la pile des appels Ltac (tout en préservant certains aspects de la récursivité terminale - cf bug #468). - Tactiques primitives - ajout de "move before" dans les tactiques primitives et ajout des syntaxes move before et move dependent au niveau utilisateur (*), - internal_cut peuvent faire du remplacement de nom d'hypothèse existant, - suppression de Intro_replacing et du code sous-traitant - Nettoyage - Suppression cible et fichiers minicoq non portés depuis longtemps. (*) Extensions de syntaxe qu'il pourrait être opportun de discuter git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques amendements liées à la compilation des packages.Gravatar herbelin2008-06-01
| | | | | | | | | | | | | | | | | | | | | - typo du configure; - warnings variables non utilisées dans ide/utils; - suppression des variables vides COQINSTALLPREFIX et OLDROOT parce que l'option -e que l'on aurait pu en principe utiliser pour les surcharger ne fonctionne pas lorsqu'il y a plusieurs niveaux d'imbrication de makefiles (comme c'est le cas quand on vient du makefile servant à faire les packages qui appelle le makefile principal qui appelle les makefile.stage); - utilisation de ALLVO plutôt qu'un find pour trouver les .v sur lesquels appliquer coqdep (permet d'éviter des warning sur les fichiers de test, non prévus pour faire partie de la biblio standard); - utilisation de -custom sur les bytecode qui ne l'étaient pas encore (coqchk et coqmktop) pour être indépendant de ocamlrun à l'installation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Should fix the dependancy issue mentioned by J.Forest about NMake: Gravatar letouzey2008-05-22
| | | | | | | | | .v.d are created exactly for all $(VFILES), which was only a "find -name .v", so $(GENVFILES) should be added to $(VFILES) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10965 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integration of theories/Ints into theories/Numbers, again : better ↵Gravatar letouzey2008-05-08
| | | | | | | | | | | | generation of NMake.v - genN.ml becomes NMake_gen.ml - no need to produce the corresponding binary: we use ocaml NMake_gen.ml > NMake.v - beware! redoing a ./configure is mandatory after this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10903 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integration of theories/Ints into theories/Numbers, part 3: auto-generation ↵Gravatar letouzey2008-05-08
| | | | | | of NMake.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10902 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plongement de doc/Makefile dans la nouvelle architecutre des MakefileGravatar notin2008-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10570 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implement KEEP_ML4_PREPROCESSED option in build systemGravatar lmamane2008-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10561 85f007b7-540e-0410-9357-904b9bb8a0f7
* Détection plus souple et message un peu moins radical en cas deGravatar herbelin2008-02-06
| | | | | | | fichiers emacs ouverts au moment de la création des dépendances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10519 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration de la génération des graphes de dépendancesGravatar notin2008-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10438 85f007b7-540e-0410-9357-904b9bb8a0f7
* migration of ide/utf8.v to theories/Unicode/Utf8.vGravatar letouzey2007-12-13
| | | | | | | | | | | | | | | | | | These notations aren't CoqIDE-specific, I can now use them with ProofGeneral (after a small modification of PG, contact me if you're interested by the patch). So let's place this file in a globally visible subdir of theories/. By the way, the filename is now uppercase as all other .v files. By the way, minor other changes in Makefile : extraction/test doesn't exist anymore, and tags / otags can be made without re-doing any find. NB: be sure to use etags that comes from emacs and not the one of exuberant-ctags, since the latter has now a different syntax (in debian, see update-alternatives etags). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10376 85f007b7-540e-0410-9357-904b9bb8a0f7
* build system: When using GOTO_STAGE, always go into that stage, even when ↵Gravatar lmamane2007-10-15
| | | | | | target already exists git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10223 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow a few build system optimisations/corner-cuttingGravatar lmamane2007-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10218 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add glob.dump to Makefile the recommended way and document theGravatar lmamane2007-07-25
| | | | | | | recommended way more explicitly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10050 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications de la construction de la documentation de la librairieGravatar notin2007-07-25
| | | | | | | | | | | | | standard: - ajout d'une entrée dans le Makefile principal pour le fichier de globalisations glob.dump - modifications de doc/Makefile et de l'index html pour gérer les nouveaux fichiers de la librairie standard (en part. ceux dans Ints) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanly refuse to operate in the presence of unsaved changes in emacsGravatar lmamane2007-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10025 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not try to clean the doc when no config/MakefileGravatar lmamane2007-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10013 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorganise cleaning targetsGravatar lmamane2007-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10012 85f007b7-540e-0410-9357-904b9bb8a0f7
* A cleaner solution to "make deletes .ml4.d files -> infinite loop" problemGravatar lmamane2007-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10010 85f007b7-540e-0410-9357-904b9bb8a0f7
* New bootstrapping, improved, Makefile systemGravatar corbinea2007-07-13
| | | | | | | Documented in dev/doc/build-system.txt . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9992 85f007b7-540e-0410-9357-904b9bb8a0f7
* (Port of r9984) Easier debugging:Gravatar glondu2007-07-12
| | | | | | | | | * explicitation of some types * tags for grammar entries git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot to commit new MakefileGravatar msozeau2007-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9975 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petites corrections sur le MakefileGravatar notin2007-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9965 85f007b7-540e-0410-9357-904b9bb8a0f7
* Missing include path of ocaml .h when generating depsGravatar msozeau2007-07-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9930 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added the directory theories/Numbers where axiomatizations and ↵Gravatar emakarov2007-06-29
| | | | | | implementations (unary, binary, etc.) of different number classes (natural, integer, rational, real, complex, etc.) will be stored.Currently there are axiomatized natural numbers with two implementations and axiomatized integers. Modified Makefile accordingly but dod not include the new files in THEORIESVO yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9916 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplification de la construction du .depend:Gravatar notin2007-06-21
| | | | | | | | | | - make ou make world entraînent la construction de .depend et .depend.coq; - suppression des cibles .depend et .depend.coq (au profit de depend et dependcoq) - suppression de la dépendance de depend avec les .ml (inutile) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9904 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding: Field instance for Q.Gravatar roconnor2007-06-21
| | | | | | | | : Power function from Q -> Z -> Q. : Absolute value function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9901 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug sur make dependGravatar notin2007-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9889 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various Program fixes, multiple pattern matches, aliases. Fix bug in ↵Gravatar msozeau2007-06-09
| | | | | | | | | | coercion code for simultaneous coercion of different arguments of an inductive type. Add tactics for dealing with heterogeneous equality. Export more error reporting functions from Cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9886 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | apply afin de reculer au plus tard les décisions irréversibles et en particulier de pouvoir typer les with-bindings modulo coercions : - l'unification des types des métas données en with-bindings est retardé à après l'unification (unify_0) de telle sorte que les instances trouvées par unify_0 soient prioritaires et que la décision d'insérer éventuellement des coercions autour des valeurs données en with-bindings se fasse au dernier moment; - toujours pour permettre d'insérer ultimement des coercions, l'instantiation des with-bindings ne se fait plus l'appel unify_0 (cf clenv_unique_resolver); - pour permettre ce retardement sans limiter le test de conversion que unify_0 fait sur les termes clos, on transmet à unify_0 les métas données en with-bindings (ainsi l'instantiation de ces métas peut être faite dynamiquement au moment du test de clôture); - parce que les métas données en with-bindings qui sont en position de rédex (cas d'un "apply f_equal with (f:=fun ...)" peuvent simplifier le problème d'unification (et elles ne sont pas de toutes façons pas réinférables au premier ordre), on continue à les substituer avant l'appel à unify_0 (cf meta_reducible_instance); - pour l'unification du second-ordre, on continue d'instancier les with-bindings et d'unifier les types des with-bindings avant unification; - reste à régler un problème de compatibilité lorsque le résultat de l'unification des types des with-bindings est utilisé pour rendre un terme clos et pour permettre à unify_0 d'utiliser la conversion. + meilleure compatibilité de apply, split, left, right pour le code qui l'utilise avec des bindings clos + nettoyage et uniformisation des clenv_match_args, clenv_missing, et assimilés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9850 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added Z and Q implementations with int31.Gravatar aspiwack2007-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9846 85f007b7-540e-0410-9357-904b9bb8a0f7
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
| | | | | | | | | details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
* On n'a plus besoin de compiler les anciens fichiers de functionnal induction ↵Gravatar jforest2007-04-05
| | | | | | (version P.Courtieu). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9748 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications dans Makefile: Gravatar notin2007-03-30
| | | | | | | | | make et make world déclenchent maintenant la compilation des dépendances. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9736 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout contrib/dp/Dp.voGravatar filliatr2007-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9721 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug dans Makefile (COQINSTALLPREFIX)Gravatar notin2007-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9702 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug de l'install (win)Gravatar notin2007-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9680 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix mistake naming my Tactics file Tactics :)Gravatar msozeau2007-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9624 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add tactics for induction on subterms.Gravatar msozeau2007-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9623 85f007b7-540e-0410-9357-904b9bb8a0f7
* complement du commit 9591Gravatar bgregoir2007-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9592 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated Makefile to include ConstructiveEpsilon.vGravatar emakarov2007-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9523 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move definition of VO_TOOLS_DEP before first use of it.Gravatar lmamane2007-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9498 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reintroduce compatibility with old versions of GNU makeGravatar lmamane2007-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite au mail de Lionel a propos du Makefile: Gravatar letouzey2007-01-12
| | | | | | | | | | | | | | | | | 1) Disparition de test_extraction.v rebasculé dans test-suite/success/extraction.v Au passage, remplacement de quelques Set en Type pour ne pas avoir besoin du -impredicative-set. Et ajout de passes d'extraction en Haskell et Scheme. Simplification du Makefile en conséquence (plus de barestate) 2) Au passage, reparation (et embellissement) de extract_env. Depuis le passage de Claudio dans cette portion (il y a 2 ans ?), faire Extraction S (ou tout autre constructeur) echouait. Idem pour un nom d'inductif mutuel autre que le premier du paquet. Etonnant que personne n'ait remarqué ca plus tot... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9484 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Make .vo files depend on coqdoc if COQ_XML is set (bug #848)Gravatar lmamane2007-01-10
| | | | | | | | - Clean up NO_RECOMPILE_LIB treatment a bit - Clean up .vo dependencies in general git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9478 85f007b7-540e-0410-9357-904b9bb8a0f7