aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
Commit message (Collapse)AuthorAge
* 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
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - Makefile: Option (environment variable NO_RECOMPILE_LIB) to not recompile the whole standard library just because the coq binaries got rebuilt. - Infrastructure to change the object pretty-printers at runtime. - Use that infrastructure to make coqtop-protocol with Pcoq trees and Pcoq-protocol with pretty-printed terms possible in coq-interface. - Make "Back(track)" into closed sections, modules and module types "Just Work™". - Modernise/generalise Pcoq protocol a bit, make some of its warts optional. - Implement "Show." in Pcoq mode. - Add Rpow_def.vo to REALSBASEVO so that its dependencies are computed (and used). - "make revision" now handles GNU Arch / tla in addition to svn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9476 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subtac fixes, support for reasoning on wf defs.Gravatar msozeau2007-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9473 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptation à Subversion 1.4Gravatar notin2006-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9457 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans le kernel : Gravatar bgregoir2006-12-11
| | | | | | | | | | | | | | | | | | | | | - essai de suppression des dependances debiles. (echec) - Application des patch debian. Pour ring et field : - introduciton de la function de sign et de puissance. - Correction de certains bug. - supression de ring_replace .... Pour exact_no_check : - ajout de la tactic : vm_cast_no_check (t) qui remplace "exact_no_check (t<: type of Goal)" (cette version forcais l'evaluation du cast dans le pretypage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
* dpGravatar filliatr2006-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9419 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fork of cases impl for subtac.Gravatar msozeau2006-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9407 85f007b7-540e-0410-9357-904b9bb8a0f7
* The $(BEST) binaries symlinks depend on existence of target, not newness.Gravatar lmamane2006-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9405 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptation à FreeBSDGravatar notin2006-11-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9378 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit polymorphismeGravatar herbelin2006-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte dépendance de subtyping en typeops (polymorphisme de defs)Gravatar herbelin2006-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9311 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9302 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout ListTacticsGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9291 85f007b7-540e-0410-9357-904b9bb8a0f7
* Experimental merging of two functional graphs.Gravatar courtieu2006-10-26
| | | | | | | temporary synatx: Mergeschemes (G1 a b c) with (G2 a d e) using G1G2. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9285 85f007b7-540e-0410-9357-904b9bb8a0f7
* conflit de nom (Field_theory) modulo la casseGravatar barras2006-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9273 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en forme des theoriesGravatar notin2006-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option -annotate au configure+ changement du comportement par ↵Gravatar notin2006-10-11
| | | | | | défaut de make git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9232 85f007b7-540e-0410-9357-904b9bb8a0f7
* separation de RealFieldGravatar barras2006-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9187 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile : COQLIB -> FULLCOQLIBGravatar corbinea2006-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9183 85f007b7-540e-0410-9357-904b9bb8a0f7
* petits pbs de dependancesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9181 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compilation newringGravatar notin2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9180 85f007b7-540e-0410-9357-904b9bb8a0f7
* commit de field + renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1215Gravatar notin2006-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9149 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix wrong order for building library, add informative messages.Gravatar msozeau2006-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subtac fixes, new way of handling obligations in progress.Gravatar msozeau2006-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9117 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification du configure pour paramétrer les exécutables liés à la ↵Gravatar notin2006-08-30
| | | | | | compilation C git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de l'appel aux exécutables Caml (noms absolus)Gravatar notin2006-08-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9095 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications dans les scripts de configuration (coqtop et coqide affichent ↵Gravatar notin2006-07-28
| | | | | | maintenant le numéro de révision svn) + correction problème OCaml 3.07 et caml_;odify git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9063 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification script sed pour compatibilité WindowsGravatar notin2006-07-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9059 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
| | | | | | | | | | | | | | | | | | | Part contre ces cas sont detruis dans les "Definition" (pas dans les "Lemma") je comprends pas ou ils sont enlev'e... Si une id'ee ... - Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland. - Meilleur compilation des coinductifs, on utilise maintenant vraimment du lazy. - Enfin un peu plus de doc dans le code de la vm. Benjamin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retrait du -noassert qui etait present en natif. Gravatar letouzey2006-07-13
| | | | | | | | | | | | | Ce -noassert empechait par exemple de s'apercevoir d'un echec actuel dans la test-suite. Heureusement les paquets debian faits par Samuel Mimram sont testés sur des tas d'archis, dont certaines en bytecode, ce qui a permis de reperer le bug. Pour que de telles blagues ne se reproduisent pas, il est essentiel que les asserts soient vérifiés y compris en natif. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9049 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvel algorithme pour Zgcd (plus rapide) + un QcompareGravatar letouzey2006-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement Int.v dans ZArith, déplacement de DecidableType.v et ↵Gravatar herbelin2006-06-09
| | | | | | DecidableTypeEx.v dans Logic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8933 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ Makefile dependGravatar herbelin2006-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8928 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout exists! et restructuration/extension des fichiers sur laGravatar herbelin2006-06-04
| | | | | | | description et le choix git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8892 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de QArith dans les theories standardsGravatar letouzey2006-05-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8883 85f007b7-540e-0410-9357-904b9bb8a0f7
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
| | | | | | | | | | | | | Adds a new kind of casts (CastCoerce) for coercing an object to its base type (e.g. inductive). The new cast_type type subsumes usual casts ConvCasts. Much of the patch is just adding ConvCasts where needed. The Pretyping module has been adapted to this change, although it doesn't change anything yet, but this construct could have a use with current coercions also. Pretyping is also cleaned from the "Use type constraints under lambdas" patch which is not yet ready for wide use. It has been transferred to a copy of the Pretyping Functor in subtac_pretyping_F.ml. Subtac is now working as well as I demonstrated at TYPES. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8875 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de la compilation de coqc et coqmktop pour éviter le problème ↵Gravatar notin2006-05-26
| | | | | | de stripping automatique sous Fedora git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8865 85f007b7-540e-0410-9357-904b9bb8a0f7
* un debut de propriétés concernant FMapGravatar letouzey2006-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8844 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dépendances pour List.vGravatar notin2006-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8828 85f007b7-540e-0410-9357-904b9bb8a0f7
* etoffage des notions de permutations (a la fois List.Permutation et ↵Gravatar letouzey2006-05-16
| | | | | | Permutation.permutation) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8823 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 08:07:11 +0000