aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-09-21Remove remaining occurrences of -just-parsing.Guillaume Melquiond
2017-09-21Improve support for "-w none" compatibility option.Guillaume Melquiond
2017-09-21Handle multiple -w options on command line (bug #5736).Guillaume Melquiond
2017-09-20In gitlab set TRAVIS_BRANCH so user overlays will work as expected.Gaëtan Gilbert
2017-09-20coq_makefile: dont show errors from failed (ignored) rmdirRalf Jung
2017-09-20ssr: fix canonical strucut key comparison with primproj onEnrico Tassi
2017-09-20[flags] Flag `open Flags`Emilio Jesus Gallego Arias
2017-09-19An optimization of tactic constructor.Hugo Herbelin
2017-09-19coq_makefile: make sure compile flags for Coq and coq_makefile are in syncEmilio Jesus Gallego Arias
2017-09-19Fixing bug #5741 (anomaly in info_trivial).Hugo Herbelin
2017-09-19Merge PR #1036: Unify EConstr.t equalityMaxime Dénès
2017-09-19Improve documentation of Status message.Maxime Dénès
2017-09-19Remove STM vernaculars.Maxime Dénès
2017-09-19Add XML protocol support for Wait.Maxime Dénès
2017-09-19Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).Maxime Dénès
2017-09-19Merge PR #1043: Disable OSX signing for temporary artifacts.Maxime Dénès
2017-09-19Document UState.universe_context.Gaëtan Gilbert
2017-09-19Don't lose names in UState.universe_context.Gaëtan Gilbert
2017-09-19test-suite: polymorphismMatthieu Sozeau
2017-09-19proof_global: cleanup and comment close_proofMatthieu Sozeau
2017-09-19Allow declaring universe binders with no constraints with @{|}Gaëtan Gilbert
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-09-19Allow empty instance parsing @{}Matthieu Sozeau
2017-09-19Merge PR #1024: Switch Travis to OSX 10.12 and Xcode 8.3.3.Maxime Dénès
2017-09-19Merge PR #920: kernel: bugfix in filter_stack_domain.Maxime Dénès
2017-09-18Reporting locations in error messages about notation formats.Hugo Herbelin
2017-09-18Fixing two anomalies in corner cases of the syntax of notation formats.Hugo Herbelin
2017-09-18Add test-suite script by Cyprien ManginMatthieu Sozeau
2017-09-15Merge PR #979: Fix install-doc target and other gitlab failuresMaxime Dénès
2017-09-15Fix CHANGES after merge of PR #1025.Théo Zimmermann
2017-09-15Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...Maxime Dénès
2017-09-15Merge PR #1051: Using an algebraic type for distinguishing toplevel input fro...Maxime Dénès
2017-09-15Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Maxime Dénès
2017-09-15Merge PR #1046: Better error messages, fix for BZ#5723Maxime Dénès
2017-09-15Merge PR #1045: Remove unneeded fix for BZ#1715Maxime Dénès
2017-09-15Merge PR #1042: Fixing minor typos in stm/coqideMaxime Dénès
2017-09-15Merge PR #1000: Update CREDITS on a best-effort basis.Maxime Dénès
2017-09-15Merge PR #1037: Parse directly to Sorts.family when appropriate.Maxime Dénès
2017-09-15Merge PR #1025: BZ#5716, read flags from project file for Compile BufferMaxime Dénès
2017-09-15Add debug output to brew update.Maxime Dénès
2017-09-15Switch Travis to OSX 10.12 and Xcode 8.3.3.Maxime Dénès
2017-09-15Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...Maxime Dénès
2017-09-15Merge PR #990: Prevent warning about DSTROOT being undefined.Maxime Dénès
2017-09-15Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...Maxime Dénès
2017-09-15Merge PR #962: Move dev/doc/changes to Markdown.Maxime Dénès
2017-09-15Merge PR #955: Do not hashcons universes beforehandMaxime Dénès
2017-09-15Merge PR #938: [parsing] Remove hacks for reduced Prelude.Maxime Dénès
2017-09-15Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match anon...Maxime Dénès
2017-09-14Using an algebraic type for distinguishing toplevel input from location in file.Hugo Herbelin
2017-09-14Avoid extra failure in the "constructor" tactic (bug #5666).Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-19 06:37:05 +0000