aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2015-03-26allows the vm to deal with inductive type with 8388607 constant constructors ...Benjamin Gregoire
2015-03-26fix compilationBenjamin Gregoire
2015-03-26Fix bug 4157,Benjamin Gregoire
2015-03-26add coqdep in distributed_exec, else make does not work.Benjamin Gregoire
2015-03-26STM: change how proof mode switching commands are handled (decl_mode)Enrico Tassi
2015-03-25Fix vm compiler to refuse to compile code making use of inductives withMatthieu Sozeau
2015-03-25More clever representation of substituted Cemitcode.Pierre-Marie Pédrot
2015-03-25Summary: fix code to detect functional values in summaryEnrico Tassi
2015-03-25STM: avoid processing asynchronously empty proofs (Close: #4134)Enrico Tassi
2015-03-25Exporting memory representation of STM tasks for votour.Pierre-Marie Pédrot
2015-03-25Fully fixing bug #3491 (anomaly when building _rect scheme in theHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 09:16:01 +0000