aboutsummaryrefslogtreecommitdiff
path: root/tools
AgeCommit message (Expand)Author
2014-07-24fixup fakeide test-suitePierre Boutillier
2014-07-07Coq_makefile: fix cmx compilation when there are both ml and mllibPierre Boutillier
2014-07-03Fix Coq_makefile in presence of mlpackPierre Boutillier
2014-07-03coqdoc is minimaly -Q awarePierre Boutillier
2014-07-03Bug 3405: Coq_makefile: Implicit rules only for listed files in Make filePierre Boutillier
2014-06-30Coq_makefile takes advantages of -I -Q -R cleanupPierre Boutillier
2014-06-30coqc is -Q awarePierre Boutillier
2014-06-30Coqdep: update include strategiesPierre Boutillier
2014-06-30Coq_makefile: -extra[-phony] correction + docPierre Boutillier
2014-06-25all coqide specific files moved into ide/Enrico Tassi
2014-06-16Checking that a library name is valid before compilation.Pierre-Marie Pédrot
2014-06-13Remove documentation for the unsupported options -byte and -opt.Guillaume Melquiond
2014-05-26make coqdep canonicalize paths from the command lineGregory Malecha
2014-05-17Fixing coqdep_boot warning relative to unknown ML files that were in tactics.Pierre-Marie Pédrot
2014-05-12Fixing the undocumented -dumpgraphbox option of coqdep.Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-28Reduce the amount of "Coq <" prompts generated by coq_tex. (Partial fix for b...Guillaume Melquiond
2014-04-28Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)Guillaume Melquiond
2014-04-28Recognize Parameters as a command in coqdoc. (Fix for bug #3279)Guillaume Melquiond
2014-04-28Mark lazymatch as an Ltac keyword for coqdoc. (Fix for bug #3276)Guillaume Melquiond
2014-04-28Fixing coqdoc bug #3292 (unfortunate collision betweens the relativeHugo Herbelin
2014-04-25coq_makefile: -I for the new stm/ dirEnrico Tassi
2014-04-10Dumpglob: factor out reference dumping.Carst Tankink
2014-04-09Adapt coq_makefile build rules to new -R -I semanticPierre Boutillier
2014-04-06Add tool for fully qualifying Require statements.Guillaume Melquiond
2014-04-04Recognize "Instance" in coqwc. (Fix for bug #2551)Guillaume Melquiond
2014-04-04Prevent verbatim text from leaking out of comments. (See bug #2882)Guillaume Melquiond
2014-04-04Support other forms of "Proof" in coqwc. (Fix for bug #2735)Guillaume Melquiond
2014-03-28Newline on -slash warning in coqdep.Pierre-Marie Pédrot
2014-03-12fake_ide: fix compilationEnrico Tassi
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-02Set officially the minimal OCaml requirement to 3.12.1Pierre Letouzey
2014-02-28Fix compilation of coq and plugins using coq_makefile under cygwinEnrico Tassi
2014-02-26coq_makefile: new target vi2voEnrico Tassi
2014-02-26vi2vo: new flag -schedule-vi2voEnrico Tassi
2014-02-10fake_ide: ported to spawnEnrico Tassi
2014-01-30Coqmktop without Sys.command, changes in ./configure -*byteflags optionsPierre Letouzey
2014-01-30Get rid of two utility files, obsolete now that configure is a .mlPierre Letouzey
2014-01-26-schedule-vi-checking ported to spawnEnrico Tassi
2014-01-19Using full paths in coqdep -dumpgraph.Pierre-Marie Pédrot
2014-01-19Fixing coqdep graph printing. The transitive reduction algorithm was bugged.Pierre-Marie Pédrot
2014-01-16Implementing transitive reduction in the dependency graph printingPierre-Marie Pédrot
2014-01-13Declared ML Module are not uncapitalized/capitalized/uncapitalized/...Pierre Boutillier
2014-01-06Adding a -dumpgraph option to Coqdep that output the graph dependency of thePierre-Marie Pédrot
2014-01-05Paral-ITP: cleanup of command line flags and more conservative defaultEnrico Tassi
2014-01-05coqtop: -check-vi-tasks and -schedule-vi-checkingEnrico Tassi
2014-01-04.vi files: .vo files without proofsEnrico Tassi
2013-12-22Adding -bt to coqc.Pierre-Marie Pédrot
2013-12-20coqc: execvp is now available even on win32Pierre Letouzey
2013-12-20coqmktop without Unix (simpler all_subdirs)Pierre Letouzey