aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-09-22Merge PR #1070: Remove remaining occurrences of -just-parsing.Maxime Dénès
2017-09-22Merge PR #1064: coq_makefile: dont show errors from failed (ignored) rmdirMaxime Dénès
2017-09-22Merge PR #1063: [flags] Flag `open Flags`Maxime Dénès
2017-09-22Merge PR #1061: Fix appveyor buildMaxime Dénès
2017-09-21Report missing arguments in error messageTej Chajed
2017-09-21Properly handle "coq_makefile -Q . Foo" (bug #5580).Guillaume Melquiond
2017-09-21Fix -silent flag of coqchk after ff918e4.Maxime Dénès
2017-09-21Adapt checker to change in locations.Maxime Dénès
2017-09-21Proposing meta names more distinguishable from evar names than ?M42.Hugo Herbelin
2017-09-21A possible fix to BZ#5750 (ability to print context of ltac subterm match).Hugo Herbelin
2017-09-21[checker] Add missing Feedback printer (BZ#5587)Emilio Jesus Gallego Arias
2017-09-21Do not run Travis OS X packaging job on PRsThéo Zimmermann
2017-09-21Do not reinstall preinstalled packages under AppVeyor.Maxime Dénès
2017-09-21Print Cygwin setup output rather than logging in to a file.Maxime Dénès
2017-09-21Mark "Set Tactic Compat Context" as deprecated.Guillaume Melquiond
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