aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
Commit message (Collapse)AuthorAge
* Amélioration de coq_makefileGravatar notin2009-02-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11945 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report des revisions #11826, #11828 et #11829 de v8.2 vers trunkGravatar notin2009-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11915 85f007b7-540e-0410-9357-904b9bb8a0f7
* From v8.2 to trunk:Gravatar herbelin2009-02-06
| | | | | | | | | - commit 11871 (Miller's pattern detection bug) + a corresponding test - commit 11883 (.ml4 to .cmxs in coq_makefile) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11884 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix d'un bug avec l'option gallinaGravatar notin2009-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11880 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Better deal with commands inside section titles in latex output usingGravatar msozeau2009-01-21
| | | | | | | | the support from hyperref. - Rename n-ary 'exist' tactic to 'exists' in Program.Syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various little fixes:Gravatar msozeau2009-01-18
| | | | | | | | | | | | - allow a new line after a (** printing *) directive in coqdoc so as not to output spurious new lines. - never directly unify the lemma with an evar in setoid_rewrite (they act as opaque constants). - Fix a useless dependency introduced by tauto which splits a record in SetoidList. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11799 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patch by Brian Campbell to output more information on the exception thatGravatar msozeau2009-01-15
| | | | | | | made a glob file unreadable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11788 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oups... il n'y a pas d'option -impl pour ocamldepGravatar notin2009-01-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11771 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor doc fixes:Gravatar msozeau2009-01-08
| | | | | | | | | | | - Set BIBINPUTS variable correctly so that we do not use any random biblio.bib file. - Update setoid_rewrite doc to new typeclasses syntax and fix verb -> texttt - Stop using less than 100% line heights in coqdoc.css git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11767 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sous Windows, 'coqtop -where' renvoit des chemins contenant des '\'Gravatar notin2009-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite de la révision #11756Gravatar notin2009-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11757 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added installation of .cmi files in "make install" target of coq_makefile.Gravatar herbelin2009-01-04
| | | | | | | | Updated CHANGES. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11747 85f007b7-540e-0410-9357-904b9bb8a0f7
* Produce better html code with coqdoc and improve doc:Gravatar msozeau2008-12-29
| | | | | | | | | | - correct nesting of a and div (fixes bug #2022) - use span instead of div for inline parts - fix standard lib template missing/new links - use -g to produce the stdlib doc (no proofs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11724 85f007b7-540e-0410-9357-904b9bb8a0f7
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
| | | | | | | | | | | | | of the archive to install in coq user-contrib installation directory. - Relaxed the validity check on identifiers from an error to a warning. - Added a filtering option to Print LoadPath. - Support for empty root in option -R. - Better handling of redundant paths in ml loadpath. - Makefile's: Added target initplugins and added initplugins to coqbinaries. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | principaux changements sont: - coqtop (et coqc) maintenant insensible aux variables d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les librairies Coq peut être spécifié par l'option -coqlib - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les chemins des exécutables OCaml; en dehors du mode boot, coqmktop cherche les exécutables OCaml dans PATH - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci étant installé en copiant l'architecture des sources (ie lib.cmxa est installé dans COQLIB/lib/lib.cmxa) - coq_makefile prend maintenant 3 paramètres sous forme de variables d'environnement: COQBIN pour dire où trouver les exécutables Coq, CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les chemins vers les librairies sont déduits en utilisant -where Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de simuler les conditions de la vie réelle (Ocaml pas dans le PATH, installation binaire relocalisée, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Take advantage of natdynlink when available: almost all contribs become ↵Gravatar letouzey2008-12-16
| | | | | | | | | | | | | | | | | | | | | | | | loadable plugins - Any contrib foo leads to contrib/foo/foo_plugin.cmxs (and .cma for bytecode). - Features that were available without any Require are now loaded systematically when launching coqtop (see Coqtop.load_initial_plugins): extraction, jprover, cc, ground, dp, recdef, xml - The other plugins are loaded when a corresponding Require is done: quote, ring, field, setoid_ring, omega, romega, micromega, fourier - I experienced a crash (segfault) while turning subtac into a plugin, so this one stays statically linked into coqtop for now - When the ocaml version doesn't support natdynlink, or if "-natdynlink no" is explicitely given to configure, coqtop is statically linked with all of the above code as usual. Some messages [Ignore ML file Foo_plugin] may appear. - How should coqdep handle a "Declare ML Module "foo"" if foo is an archive and not a ml file ? For now, we suppose that the foo.{cmxs,cma} are at the same location as the .v during the build, but can be moved later in any place of the ml loadpath. This is clearly an experimentation. Feedback most welcome... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11687 85f007b7-540e-0410-9357-904b9bb8a0f7
* - configure: do not strip coqtop on Darwin so as to support dynamic loadingGravatar herbelin2008-12-12
| | | | | | | | | | | - configure: remove useless newline (hoping it is OK for everyone) - coqc: added option -no-glob in accordance with coqc -usage - coq_makefile: support for installation of all .cmo and all .cmxs in user-contrib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11676 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Synchronized subst_object with load_object (load_and_subst_objects)Gravatar herbelin2008-11-23
| | | | | | | | | | | | | | | | | | and set Declare ML Module as a regular substitutive object so that Declare ML Module is treated at the right place in the order of appearance of substitutive declarations of a required module. - Note: The full load/import mechanism for modules is not so clear: the Require part of a Require Import inside a module is set outside the module at module closing but the Import part remains inside (why not to put the "special" objects in the module too?); moreover the "substitute" and "keep" objects of a module are desynchronised at module closing (is that really harmless/necessary?). - Treatment of .cmxs targets in coq_makefile and in coqdep. - Better make clean in coq_makefile generated makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug in VernacExtend printing + missing vernacular printing rules +Gravatar herbelin2008-11-22
| | | | | | | | | | revival of option -translate as a -beautify option. PS: compilation checked against 11610. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11618 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration du README.doc et de l'installation de la docGravatar notin2008-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative d'amélioration de la robustesse des Makefile générés parGravatar notin2008-11-13
| | | | | | | | | | | | | | | | coq_makefile en présence de fichiers .ml : - ajout d'une option -config à coqtop qui affiche les informations de configuration (COQTOP, COQBIN, COQLIB, CAMLP4, CAMLP4LIB, CAMLBIN, LOCAL) - coq_makefile inclut un fichier Makefile.config qui contient les valeurs des variables sus-mentionnées git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11584 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite #11533Gravatar notin2008-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11554 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1926Gravatar notin2008-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11553 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un petit bug en cas de redéfintion par l'utilisateur de ↵Gravatar notin2008-11-06
| | | | | | variables utilisées dans PP git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11546 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes:Gravatar msozeau2008-11-05
| | | | | | | | | - Rework definition of the type of respecful functions in Morphisms.v - Unfold [flip] in "Add Morphism" tactic (suggested by N. Tabareau) - Add a "coqvariableref" command in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11545 85f007b7-540e-0410-9357-904b9bb8a0f7
* 2 petites améliorations de coq_makefile (traitement des .ml4 + cibles ↵Gravatar notin2008-11-04
| | | | | | génériques dans -custom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11535 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option -raw pour Coqdoc (sortie en texte brut)Gravatar notin2008-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11529 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stop using a coqdocdoc env which prevents use of environments insideGravatar msozeau2008-10-26
| | | | | | | | | comments that go across code and doc (e.g. for beamer frames), it was unused anyway. Add "do" and "repeat" as tactic identifiers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11507 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various coqdoc improvements:Gravatar msozeau2008-10-22
| | | | | | | | | | | | | - New "color" option to the coqdoc latex style file to typeset using the xcolor package, still following the McBride convention. - Work on proper indentation and spacing of output code and allow users to customise indentation (setting a base indentation length) and line skips for empty lines of code. - Also add new environments to distinguish code and documentation, doing nothing right now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11491 85f007b7-540e-0410-9357-904b9bb8a0f7
* Syntaxe de COQBINGravatar notin2008-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11475 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)Gravatar herbelin2008-10-18
| | | | | | | | | - Makefile: typo apparente avec .ml4.preprocessed - test-suite: ajout d'un test sur eta qui trainait dans le coin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11465 85f007b7-540e-0410-9357-904b9bb8a0f7
* ## Lines starting with '## ' will be removed from the log message.Gravatar msozeau2008-10-06
| | | | | | | | | | | | | | | | ## File(s) to commit: ## tools/coqdoc/index.mll ## tools/coqdoc/output.ml ## tools/coqdoc/pretty.mll Various improvements to coqdoc: - (Hopefully) better handling of brackets and notations like \in (debugger with Stéphane Lescuyer). - More indexed tactics and commands. - Fix bug(?) in parsing of "[[" comments. - Better interpolation of module and library names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11432 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes related to coqdoc and --interpolate and the dependentGravatar msozeau2008-10-03
| | | | | | | induction test-suite script. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot one file.Gravatar msozeau2008-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11422 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improvements in coqdoc:Gravatar msozeau2008-09-25
| | | | | | | | | | | | | | | | - Better handling of spaces by actually ignoring what's inside proof scripts in light/gallina mode (detection of [Proof with] vs [Proof.] vs [Proof t.] and [Qed]/[Save]/...). - Provide fancy replacements for forall,/\,... etc in HTML in case the utf8 option is on. - Use typesetting information in HTML output and customize the CSS accordingly. The default color scheme follows closely the one set by Conor for Epigram; of course one can change it. - A try at interpolating identifiers in comments if they are defined in the same module, with a corresponding flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11421 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add types introduced by subtac in *.glob filesGravatar glondu2008-09-15
| | | | | | Hints from compilation warnings git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11412 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1908 (améliorations de coqdoc.css)Gravatar notin2008-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11361 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite 11266 (warning tools/gallina.ml)Gravatar herbelin2008-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11267 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from ↵Gravatar notin2008-07-18
| | | | | | de coqdoc (compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage intempestif d'information de globalisation + numéro de version ↵Gravatar notin2008-07-18
| | | | | | dans coq_makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11234 85f007b7-540e-0410-9357-904b9bb8a0f7
* - coqdoc: correction d'un bug sur les commentaires imbriquésGravatar notin2008-07-17
| | | | | | | | - coq_makefile: amélioration des chemins de camlp4/5 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11231 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli lors de la révision #11177Gravatar notin2008-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11179 85f007b7-540e-0410-9357-904b9bb8a0f7
* Création du fichier dumpglob.ml, qui rassemble les fonctions de ↵Gravatar notin2008-06-25
| | | | | | globalisation (add_glob* et dump_*) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'option -dump-glob et ajout d'une option -no-globGravatar notin2008-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11167 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code cleanup in typeclasses, remove dead and duplicated code.Gravatar msozeau2008-06-21
| | | | | | | Change from named_context to rel_context for class params and fields. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11163 85f007b7-540e-0410-9357-904b9bb8a0f7
* Little fixes: print unbound variable in error message (patch by SamuelGravatar msozeau2008-06-19
| | | | | | | | Bronson), some keywords in coqdoc, and test well-typedness of predicate in subtac_cases after abstraction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11153 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
| | | | | | | | (résolution entre autres des bugs 1882, 1883, 1884). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11145 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
| | | | | | | | | | | | | | disambiguate syntax: [ H := [ ?x ] : context C [ foo ] |- _ ] is ok, as well as [ H := ?x : nat |- _ ] or [H := foo |- _ ], but [ H := ?x : context C [ foo ] ] will not parse. Add applicative contexts in tactics match, to be able to match arbitrary partial applications, e.g.: match f 0 1 2 with appcontext C [ f ?x ] => ... end will bind C to [ ∙ 1 2 ] and x to 0. Minor improvements in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11129 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un problème lié à une interaction entre hyperref etGravatar notin2008-06-12
| | | | | | | | | | | | | latex, qui empechait de produire des fichiers .dvi à partir des .tex générés par coqdoc. --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M trunk/tools/coqdoc/coqdoc.sty M branches/v8.2/tools/coqdoc/coqdoc.sty git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11120 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de l'export des .cmi dans coq_makefileGravatar notin2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11106 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 02:56:09 +0000