Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | | | | | | | | | | | | | | | | | | | | * | | | Fixing part of #5707 (allowing destruct to use non dependent case analysis). | 2017-08-30 | ||
| | | | | | | | | | | | | | | | | | | | | | | | * | | | Fixing a capitalization in the middle of the sentence of an error message. | 2017-08-30 | ||
| | | | | | | | | | * | | | | | | | | | | | | | | | | | mention issue with OCAMLRUNPARAM and ocamldebug | 2017-08-29 | ||
| | * | | | | | | | | | | | | | | | | | | | | | | | | | coq_makefile: fix .merlin generation (FLG -thread) | 2017-08-29 | ||
| | * | | | | | | | | | | | | | | | | | | | | | | | | | coq_makefile: improve documentation | 2017-08-29 | ||
| | * | | | | | | | | | | | | | | | | | | | | | | | | | coq_makefile: print error message when coqlib is not set properly | 2017-08-29 | ||
| | * | | | | | | | | | | | | | | | | | | | | | | | | | coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxs | 2017-08-29 | ||
| | | * | | | | | | | | | | | | | | | | | | | | | | | | Fix link to debugging file. | 2017-08-29 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | * | [general] Merge parsing with highparsing, put toplevel at the top of the link... | 2017-08-29 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | * | [vernac] Store Infix Modifier in Vernac Notation. | 2017-08-29 | ||
| | | | | | | | | | | | | | | | | | | | | |_|_|_|_|/ | | | | | | | | | | | | | | | | | | | | |/| | | | | | ||||
| | | * | | | | | | | | | | | | | | | | | | | | | | | Adapt debugging doc to configure/Makefile changes. | 2017-08-29 | ||
| | | * | | | | | | | | | | | | | | | | | | | | | | | Move debugging to Markdown. | 2017-08-29 | ||
| | | | |_|_|_|_|_|/ / / / / / / / / / / / / / / / | | | |/| | | | | | | | | | | | | | | | | | | | | | ||||
* | | / | | | | | | | | | | | | | | | | | | | | | | Fix deployment to multiple providers. | 2017-08-29 | ||
| |_|/ / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #961: Add a set of contributing guidelines | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | | | | | | | | | | | | | Avoid running interactive tests on Windows. | 2017-08-29 | ||
| | | | | | | | | | | | | | * | | | | | | | | | | | Statically enforcing that module types have no retroknowledge. | 2017-08-29 | ||
| | | | | | | | | | | | | | * | | | | | | | | | | | Separating the module_type and module_body types by using a type parameter. | 2017-08-29 | ||
| | | | | | | | | | | | | | | | | | | * | | | | | | [parsing] Remove hacks for reduced Prelude. | 2017-08-29 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | | | | | | | | | | | Properly handling parameters of primitive projections in cctac. | 2017-08-29 | ||
| | | | | | | | | * | | | | | | | | | | | | | | | Fix BZ#5697: Congruence does not work with primitive projections. | 2017-08-29 | ||
| | | | | | | | | | |_|_|_|/ / / / / / / / / / | | | | | | | | | |/| | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170 | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #988: Fix obsolete description of real numerals. | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | * | | | | | Move dev/doc/changes to Markdown. | 2017-08-29 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | Post-merge API fix. | 2017-08-29 | ||
* | | | | | | | | | | | | | | | | | | | | | | | Merge PR #946: Functional pretyping interface | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #937: [general] Remove spurious dependency of highparsing on toplevel. | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur... | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #838: Have coq-dpdgraph ci test print the differences | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #830: Moving assert (the "Cut" rule) to new proof engine | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #819: Cleanup old things | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #805: Functional tactics | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #773: [flags] Remove XML output flag. | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #966: Makefile : ignore user-contrib in various file searches | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | * | | | | | | | | | | | | | | | | | | coq_makefile: do not overwrite CAMLFLAGS | 2017-08-29 | ||
| | | | | | | | | | | | | * | | | | | | | | | | | | | | | | | | coq_makefile: use dedicated variable for extra packages | 2017-08-29 | ||
| | | | | | | | | | | | | * | | | | | | | | | | | | | | | | | | coq_makefile: build/use .cma for packed plugins | 2017-08-29 | ||
| | | | | | | | | | | | | * | | | | | | | | | | | | | | | | | | coq_makefile: test using findlib's package | 2017-08-29 | ||
| | | | | | | | | | | | | * | | | | | | | | | | | | | | | | | | test-suite: depend on byte compilation too | 2017-08-29 | ||
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #985: Fix coqdoc test-suite target on Windows. | 2017-08-29 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Trying to fix deployment of master on bintray, and deploy tags to github. | 2017-08-29 | ||
* | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Master now deploys 8.8+alpha. | 2017-08-29 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | | | | | * | | | | | | coqdoc: Support comments in verbatim output | 2017-08-29 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | * | | | | | | | | | | | | | | | | | | | | | Quoting notations in incompatible-level error message. | 2017-08-29 | ||
| | | | | | | | * | | | | | | | | | | | | | | | | | | | | | A new step of restructuration of notations. | 2017-08-29 | ||
| | | | | | | | * | | | | | | | | | | | | | | | | | | | | | Adding a test for #5569 (warning about skipping spaces). | 2017-08-29 | ||
| | | | | | | | * | | | | | | | | | | | | | | | | | | | | | Dropping former fix to bug #5469 (notation format not recognizing curly braces). | 2017-08-29 | ||
| | | | | | | | * | | | | | | | | | | | | | | | | | | | | | A little reorganization of notations + a fix to #5608. | 2017-08-29 | ||
| |_|_|_|_|_|_|/ / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | * | | | | | | | | Canonically renaming fold_map into fold_left_map in library Name. | 2017-08-29 | ||
| | | | | | | | | | | | | | | | | | | | * | | | | | | | | Adapting code to renaming Option.fold_map -> Option.fold_left_map. | 2017-08-29 | ||
| | | | | | | | | | | | | | | | | | | | * | | | | | | | | Canonically renaming fold_map into fold_left_map in library Option. | 2017-08-29 |