aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-04-06refresh metas in rewrite hints loaded from .vo files (fix bug #3815)Nickolai Zeldovich
2015-04-03Use the directory of the current session for selecting files to open.Guillaume Melquiond
2015-04-02Puts all the "import" statements first so as to accommodate the latest GHC.Nickolai Zeldovich
2015-04-02Fix some typos.Guillaume Melquiond
2015-04-02Avoid outputting stray "Local" keywords in HTML documentation.Guillaume Melquiond
2015-04-02Define Any in Haskell extraction when Tunknown is used.Nickolai Zeldovich
2015-04-02Fix compilation of documentation broken by the addition of MMapAVL.Guillaume Melquiond
2015-04-02CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)Enrico Tassi
2015-04-02Make sure that hyperref creates the proper links to the documentation indexes.Guillaume Melquiond
2015-04-02Remove Mltop.add_path as it is no longer possible to import files from subdir...Guillaume Melquiond
2015-04-02Make "Add LoadPath" behave accordingly to its documentation.Guillaume Melquiond
2015-04-02Fix documentation of -R and -Q.Guillaume Melquiond
2015-04-02Make it possible for -R to override the existing implicit setting of a path.Guillaume Melquiond
2015-04-02Display the proper error message when Require fails to find a library.Guillaume Melquiond
2015-04-02MMapAVL: some improved proofs + fix a forgotten AdmittedPierre Letouzey
2015-04-02MMapAVL: implementing MMapInterface via AVL treesPierre Letouzey
2015-04-02ZArith/Int.v: some modernizationsPierre Letouzey
2015-04-02MMapPositive: some improvementsPierre Letouzey
2015-04-01Accomodating #4166 (providing "Require Import OmegaTactic" as aHugo Herbelin
2015-04-01Fixing a few typos + some uniformization of writing in doc.Hugo Herbelin
2015-04-01More clarifications on loadpaths.Pierre-Marie Pédrot
2015-04-01Documenting "From * Require *" and clearing a bit the loadpath chapter.Pierre-Marie Pédrot
2015-04-01From X Require Y looks for X with absolute path, disregarding -R.Pierre-Marie Pédrot
2015-04-01Fixing inclusion of user contrib directory in the loadpath.Pierre-Marie Pédrot
2015-04-01Fixing test-suite.Pierre-Marie Pédrot
2015-04-01Removing a probably incorrect on-the-fly require in a tactic.Pierre-Marie Pédrot
2015-03-31Removing references to deprecated syntax -I/-R -as.Pierre-Marie Pédrot
2015-03-31Removing the unused root flag from loadpaths.Pierre-Marie Pédrot
2015-03-31Fixing test-suite.Pierre-Marie Pédrot
2015-03-31A more reasonable implementation of Loadpath.Pierre-Marie Pédrot
2015-03-31Declarative mode: fix proof modes.Arnaud Spiwack
2015-03-31Declarative mode: fix vernac classification.Arnaud Spiwack
2015-03-31Declarative mode: plug the specialised printers back.Arnaud Spiwack
2015-03-31Better formatting of messages in proofs.Arnaud Spiwack
2015-03-31Generalisation of the "end command" argument of the goal printer.Arnaud Spiwack
2015-03-31Fix various typos in documentationMatěj Grabovský
2015-03-31Do not escape "'" when outputting to html, especially not using "´".Guillaume Melquiond
2015-03-30grammar: export constr_evalEnrico Tassi
2015-03-30grammar: export hypidentEnrico Tassi
2015-03-30camlp4: grep away warnings in output/* testsEnrico Tassi
2015-03-30coq_makefile: fix compilation with camlp4Enrico Tassi
2015-03-30fix code and bound for SWITCH instruction.Benjamin Gregoire
2015-03-29Ensuring more invariants in Constr_matching.Pierre-Marie Pédrot
2015-03-29Adding test for bug #4165.Pierre-Marie Pédrot
2015-03-29Fixing bug #4165.Pierre-Marie Pédrot
2015-03-27Normalize scope names before storing them in vo files. (Fix for bug #4162)Guillaume Melquiond
2015-03-27Putting the From parameter of the Require command into the AST.Pierre-Marie Pédrot
2015-03-27STM: refine the notion of "simply a tactic"Enrico Tassi
2015-03-27Properly handle extra "clean" targets with coq_makefile.Guillaume Melquiond
2015-03-27use a more compact representation of non-constant constructorsBenjamin Gregoire
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 09:44:16 +0000