aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Remove Mltop.add_path as it is no longer possible to import files from subdir...Gravatar Guillaume Melquiond2015-04-02
* Make "Add LoadPath" behave accordingly to its documentation.Gravatar Guillaume Melquiond2015-04-02
* Fix documentation of -R and -Q.Gravatar Guillaume Melquiond2015-04-02
* Make it possible for -R to override the existing implicit setting of a path.Gravatar Guillaume Melquiond2015-04-02
* Display the proper error message when Require fails to find a library.Gravatar Guillaume Melquiond2015-04-02
* MMapAVL: some improved proofs + fix a forgotten AdmittedGravatar Pierre Letouzey2015-04-02
* MMapAVL: implementing MMapInterface via AVL treesGravatar Pierre Letouzey2015-04-02
* ZArith/Int.v: some modernizationsGravatar Pierre Letouzey2015-04-02
* MMapPositive: some improvementsGravatar Pierre Letouzey2015-04-02
* Accomodating #4166 (providing "Require Import OmegaTactic" as aGravatar Hugo Herbelin2015-04-01
* Fixing a few typos + some uniformization of writing in doc.Gravatar Hugo Herbelin2015-04-01
* More clarifications on loadpaths.Gravatar Pierre-Marie Pédrot2015-04-01
* Documenting "From * Require *" and clearing a bit the loadpath chapter.Gravatar Pierre-Marie Pédrot2015-04-01
* From X Require Y looks for X with absolute path, disregarding -R.Gravatar Pierre-Marie Pédrot2015-04-01
* Fixing inclusion of user contrib directory in the loadpath.Gravatar Pierre-Marie Pédrot2015-04-01
* Fixing test-suite.Gravatar Pierre-Marie Pédrot2015-04-01
* Removing a probably incorrect on-the-fly require in a tactic.Gravatar Pierre-Marie Pédrot2015-04-01
* Removing references to deprecated syntax -I/-R -as.Gravatar Pierre-Marie Pédrot2015-03-31
* Removing the unused root flag from loadpaths.Gravatar Pierre-Marie Pédrot2015-03-31
* Fixing test-suite.Gravatar Pierre-Marie Pédrot2015-03-31
* A more reasonable implementation of Loadpath.Gravatar Pierre-Marie Pédrot2015-03-31
* Declarative mode: fix proof modes.Gravatar Arnaud Spiwack2015-03-31
* Declarative mode: fix vernac classification.Gravatar Arnaud Spiwack2015-03-31
* Declarative mode: plug the specialised printers back.Gravatar Arnaud Spiwack2015-03-31
* Better formatting of messages in proofs.Gravatar Arnaud Spiwack2015-03-31
* Generalisation of the "end command" argument of the goal printer.Gravatar Arnaud Spiwack2015-03-31
* Fix various typos in documentationGravatar Matěj Grabovský2015-03-31
* Do not escape "'" when outputting to html, especially not using "´".Gravatar Guillaume Melquiond2015-03-31
* grammar: export constr_evalGravatar Enrico Tassi2015-03-30
* grammar: export hypidentGravatar Enrico Tassi2015-03-30
* camlp4: grep away warnings in output/* testsGravatar Enrico Tassi2015-03-30
* coq_makefile: fix compilation with camlp4Gravatar Enrico Tassi2015-03-30
* fix code and bound for SWITCH instruction.Gravatar Benjamin Gregoire2015-03-30
* Ensuring more invariants in Constr_matching.Gravatar Pierre-Marie Pédrot2015-03-29
* Adding test for bug #4165.Gravatar Pierre-Marie Pédrot2015-03-29
* Fixing bug #4165.Gravatar Pierre-Marie Pédrot2015-03-29
* Normalize scope names before storing them in vo files. (Fix for bug #4162)Gravatar Guillaume Melquiond2015-03-27
* Putting the From parameter of the Require command into the AST.Gravatar Pierre-Marie Pédrot2015-03-27
* STM: refine the notion of "simply a tactic"Gravatar Enrico Tassi2015-03-27
* Properly handle extra "clean" targets with coq_makefile.Gravatar Guillaume Melquiond2015-03-27
* use a more compact representation of non-constant constructorsGravatar Benjamin Gregoire2015-03-27
* allows the vm to deal with inductive type with 8388607 constant constructors ...Gravatar Benjamin Gregoire2015-03-26
* fix compilationGravatar Benjamin Gregoire2015-03-26
* Fix bug 4157,Gravatar Benjamin Gregoire2015-03-26
* add coqdep in distributed_exec, else make does not work.Gravatar Benjamin Gregoire2015-03-26
* STM: change how proof mode switching commands are handled (decl_mode)Gravatar Enrico Tassi2015-03-26
* Fix vm compiler to refuse to compile code making use of inductives withGravatar Matthieu Sozeau2015-03-25
* More clever representation of substituted Cemitcode.Gravatar Pierre-Marie Pédrot2015-03-25
* Summary: fix code to detect functional values in summaryGravatar Enrico Tassi2015-03-25
* STM: avoid processing asynchronously empty proofs (Close: #4134)Gravatar Enrico Tassi2015-03-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 14:43:58 +0000