aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Merge PR #1055: Remove STM vernacularsGravatar Maxime Dénès2017-09-22
|\
* \ Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as exp...Gravatar Maxime Dénès2017-09-22
|\ \
* \ \ Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a contex...Gravatar Maxime Dénès2017-09-22
|\ \ \
* \ \ \ Merge PR #1071: Mark "Set Tactic Compat Context" as deprecated.Gravatar Maxime Dénès2017-09-22
|\ \ \ \
* \ \ \ \ Merge PR #1070: Remove remaining occurrences of -just-parsing.Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \
* \ \ \ \ \ Merge PR #1064: coq_makefile: dont show errors from failed (ignored) rmdirGravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #1063: [flags] Flag `open Flags`Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #1061: Fix appveyor buildGravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \
| | | | | | * | | Proposing meta names more distinguishable from evar names than ?M42.Gravatar Hugo Herbelin2017-09-21
| | | | | | * | | A possible fix to BZ#5750 (ability to print context of ltac subterm match).Gravatar Hugo Herbelin2017-09-21
| * | | | | | | | Do not reinstall preinstalled packages under AppVeyor.Gravatar Maxime Dénès2017-09-21
| * | | | | | | | Print Cygwin setup output rather than logging in to a file.Gravatar Maxime Dénès2017-09-21
|/ / / / / / / /
| | | | * / / / Mark "Set Tactic Compat Context" as deprecated.Gravatar Guillaume Melquiond2017-09-21
| |_|_|/ / / / |/| | | | | |
| | | * | | | Remove remaining occurrences of -just-parsing.Gravatar Guillaume Melquiond2017-09-21
| |_|/ / / / |/| | | | |
| | | | * | In gitlab set TRAVIS_BRANCH so user overlays will work as expected.Gravatar Gaëtan Gilbert2017-09-20
| |_|_|/ / |/| | | |
| | * | | coq_makefile: dont show errors from failed (ignored) rmdirGravatar Ralf Jung2017-09-20
| |/ / / |/| | |
| * | | [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
|/ / /
* | | Merge PR #1036: Unify EConstr.t equalityGravatar Maxime Dénès2017-09-19
|\ \ \ | |/ / |/| |
| | * Improve documentation of Status message.Gravatar Maxime Dénès2017-09-19
| | * Remove STM vernaculars.Gravatar Maxime Dénès2017-09-19
| | * Add XML protocol support for Wait.Gravatar Maxime Dénès2017-09-19
* | | Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).Gravatar Maxime Dénès2017-09-19
|\ \ \
* \ \ \ Merge PR #1043: Disable OSX signing for temporary artifacts.Gravatar Maxime Dénès2017-09-19
|\ \ \ \
* \ \ \ \ Merge PR #1024: Switch Travis to OSX 10.12 and Xcode 8.3.3.Gravatar Maxime Dénès2017-09-19
|\ \ \ \ \
* \ \ \ \ \ Merge PR #920: kernel: bugfix in filter_stack_domain.Gravatar Maxime Dénès2017-09-19
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | |
| * | | | | Add test-suite script by Cyprien ManginGravatar Matthieu Sozeau2017-09-18
* | | | | | Merge PR #979: Fix install-doc target and other gitlab failuresGravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \
* | | | | | | Fix CHANGES after merge of PR #1025.Gravatar Théo Zimmermann2017-09-15
* | | | | | | Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #1051: Using an algebraic type for distinguishing toplevel input fro...Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #1046: Better error messages, fix for BZ#5723Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #1045: Remove unneeded fix for BZ#1715Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #1042: Fixing minor typos in stm/coqideGravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1000: Update CREDITS on a best-effort basis.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1037: Parse directly to Sorts.family when appropriate.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1025: BZ#5716, read flags from project file for Compile BufferGravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | * | | | Add debug output to brew update.Gravatar Maxime Dénès2017-09-15
| | | | | | | | | | | | * | | | Switch Travis to OSX 10.12 and Xcode 8.3.3.Gravatar Maxime Dénès2017-09-15
| |_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | |
* | | | | | | | | | | | | | | Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #990: Prevent warning about DSTROOT being undefined.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #962: Move dev/doc/changes to Markdown.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #955: Do not hashcons universes beforehandGravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #938: [parsing] Remove hacks for reduced Prelude.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match anon...Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | * | | | | | | Using an algebraic type for distinguishing toplevel input from location in file.Gravatar Hugo Herbelin2017-09-14
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | * | Avoid extra failure in the "constructor" tactic (bug #5666).Gravatar Guillaume Melquiond2017-09-14
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | Merge PR #981: Miscellaneous fixes for notationsGravatar Maxime Dénès2017-09-13
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | * | | | Fix GitLab CIGravatar Gaëtan Gilbert2017-09-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-10 00:20:32 +0000