aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
...
| | * | | 8.7 now points to Current and 8.6 points to V8_6.Gravatar Théo Zimmermann2016-09-26
| |/ / / |/| | |
| * | | The coqtop options -Q and -R do not affect the ML loadpath anymore.Gravatar Pierre-Marie Pédrot2016-09-25
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\| | |
| * | | coqc -o now places .glob file near .vo fileGravatar Enrico Tassi2016-09-22
* | | | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | | | Merge remote-tracking branch 'github/pr/283' into trunkGravatar Maxime Dénès2016-09-22
|\ \ \ \
* | | | | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
| * | | | Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Gravatar Maxime Dénès2016-09-20
| * | | | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
|/ / / /
| * | | Fix warning when using Variables at toplevel.Gravatar Maxime Dénès2016-09-19
| | * | Fix indentation of -profile-ltac in -helpGravatar Jason Gross2016-09-17
| |/ /
* | | Make the Coq codebase independent from Ltac-related code.Gravatar Pierre-Marie Pédrot2016-09-16
|\ \ \
| * | | Allowing to extend the Print Grammar command generically.Gravatar Pierre-Marie Pédrot2016-09-14
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\ \ \ \ | | |/ / | |/| |
| * | | coqc: print debug feedback coming from workersGravatar Enrico Tassi2016-09-13
| * | | Avoid putting a useless "toploop" directory in the ML search path if it does ...Gravatar Guillaume Melquiond2016-09-10
| * | | Make it explicit when paths are added to the ML search paths.Gravatar Guillaume Melquiond2016-09-09
| * | | Avoid canonizing the same paths over and over.Gravatar Guillaume Melquiond2016-09-08
| | * | Making Proof_global terminator generic in external tactics.Gravatar Pierre-Marie Pédrot2016-09-08
| | * | Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
| | * | Making Vernacexpr independent from Tacexpr.Gravatar Pierre-Marie Pédrot2016-09-08
| |/ / |/| |
* | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \
* \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\ \ \ \ | | |/ / | |/| |
| * | | Fix #4941 - ~/.coqrc file confusing locationsGravatar Maxime Dénès2016-08-30
* | | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | | | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
* | | | CLEANUP: taking advantage of "_ % _" operator to express function composition...Gravatar Matej Kosik2016-08-29
| * | | Support qualified identifiers in Show Match (bug #5050).Gravatar Guillaume Melquiond2016-08-27
* | | | Merge remote-tracking branch 'v8.6' into trunkGravatar Matej Kosik2016-08-25
|\| | |
| * | | Do not export an internal function in Namegen.Gravatar Pierre-Marie Pédrot2016-08-25
* | | | CLEANUP: removing calls of the "Context.Named.Declaration.get_value" functionGravatar Matej Kosik2016-08-25
* | | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| * | | Properly compute types for assumed section variables (bug #5035).Gravatar Guillaume Melquiond2016-08-24
| * | | Merge PR #260: "Fix bug 4842 (Time prints in multiple lines)" into v8.6Gravatar Pierre-Marie Pédrot2016-08-24
| |\ \ \
| * \ \ \ Merge PR #258: "Fix newline issues" into v8.6Gravatar Pierre-Marie Pédrot2016-08-24
| |\ \ \ \
| * | | | | Arguments: give / after last ! error detection fixedGravatar Enrico Tassi2016-08-23
| * | | | | fix get_host_port error message (#4724)Gravatar Enrico Tassi2016-08-23
|/ / / / /
* | | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
|\ \ \ \ \ | | |_|_|/ | |/| | |
| * | | | Fixing an anomaly in printing a unification error message.Gravatar Hugo Herbelin2016-08-20
| | | * | [pp] Fix bug 4842 (Time prints in multiple lines)Gravatar Emilio Jesus Gallego Arias2016-08-19
| |_|/ / |/| | |
| | | * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| | | * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
| |_|/ |/| |
| | * [pp] Fix newline issues.Gravatar Emilio Jesus Gallego Arias2016-08-19
| |/ |/|
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\|
| * Do not assume the "TERM" environment variable is always set (bug #5007).Gravatar Guillaume Melquiond2016-08-11
* | Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-29
|\|
| * Fix bug #3886, generation of obligations of fixesGravatar Matthieu Sozeau2016-07-29
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\|
| * Prevent "Load" from displaying all the intermediate subgoals.Gravatar Guillaume Melquiond2016-07-07