Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | | | | * | | | | | Merge pull request #4 from Zimmi48/patch-1 | 2017-02-20 | ||
| | | | | | | | |\ \ \ \ \ | ||||
| | | | | | | | | * | | | | | [ocamlbuild] fix small mistakes in descriptions | 2017-02-20 | ||
| | | | | | | | |/ / / / / | ||||
| | | | | | | | * | | | | | [ocamlbuild] Update meta for the vernac split. | 2017-02-20 | ||
* | | | | | | | | | | | | | Fixing debugger after the split of toplevel into vernac. | 2017-02-19 | ||
| |_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | ||||
* | | | | | | | | | | | | remove obsolete file dev/Makefile.oug | 2017-02-17 | ||
| | * | | | | | | | | | | Removing spurious folder includes in coq_makefile. | 2017-02-17 | ||
| | * | | | | | | | | | | Documenting the pluginification of Ltac. | 2017-02-17 | ||
| | * | | | | | | | | | | Fix .gitignore. | 2017-02-17 | ||
| | * | | | | | | | | | | Moving the Ltac plugin to a pack-based one. | 2017-02-17 | ||
| | * | | | | | | | | | | Ltac as a plugin. | 2017-02-17 | ||
| |/ / / / / / / / / / |/| | | | | | | | | | | ||||
| | * | | | | | | | | | Fixing #5339 (anomaly with 'pat in record parameters). | 2017-02-16 | ||
| | | | | | | * | | | | [cleanup] Change Id.t option to Name.t in TacFun | 2017-02-16 | ||
| |_|_|_|_|_|/ / / / |/| | | | | | | | | | ||||
* | | | | | | | | | | Merge PR#403: Split Vernacular Processing from Toplevel | 2017-02-16 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR#431 | 2017-02-16 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | | [travis] [External CI] CompCert official 8.6 support + UniMath | 2017-02-15 | ||
| * | | | | | | | | | | | [travis] [External CI] Factor out math-comp installs. | 2017-02-15 | ||
| | * | | | | | | | | | | Make Obligations see fix_exn | 2017-02-15 | ||
| | * | | | | | | | | | | [stm] Remove unused legacy stm interface. | 2017-02-15 | ||
| | * | | | | | | | | | | [cosmetic] Reorder makefile as suggested by @herbelin | 2017-02-15 | ||
| | * | | | | | | | | | | [stm] Reenable Show Script command. | 2017-02-15 | ||
| | * | | | | | | | | | | [stm] Break stm/toplevel dependency loop. | 2017-02-15 | ||
| |/ / / / / / / / / / |/| | | | | | | | | | | ||||
* | | | | | | | | | | | Merge PR#314: Miscellaneous fixes for Ocaml warnings. | 2017-02-15 | ||
|\| | | | | | | | | | | ||||
| * | | | | | | | | | | [unicode] Address comments in PR#314. | 2017-02-15 | ||
| * | | | | | | | | | | [safe-string] Switch to buffer to `Bytes` | 2017-02-14 | ||
| * | | | | | | | | | | [safe-string] Use `String.init` to build string. | 2017-02-14 | ||
| * | | | | | | | | | | [misc] Remove unused binding. | 2017-02-14 | ||
|/ / / / / / / / / / | ||||
* | | | | | | | | | | Merge PR#253: Sort Search results by relevance | 2017-02-14 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | Test-suite: output of Search | 2017-02-14 | ||
* | | | | | | | | | | | Merge PR#349: Proofview: tclINDEPENDENTL | 2017-02-13 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | | Proofview: tclINDEPENDENTL | 2017-02-10 | ||
|/ / / / / / / / / / / | ||||
| | | * | | | | | | | | Turning an anomaly on 'pat into a proper "unsupported" error message. | 2017-02-09 | ||
| | | * | | | | | | | | Fixing bug #5346 (an unimplemented application of 'pat). | 2017-02-09 | ||
* | | | | | | | | | | | Merge PR#405: Type cleanup in `Metasyntax` | 2017-02-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR#393: Replace Typeops with Fast_typeops | 2017-02-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* | | | | | | | | | | | | | Revert "Extraction: avoid deprecated functions of module String" | 2017-02-07 | ||
* | | | | | | | | | | | | | Extraction cosmetic: no whitespaces in printing empty modules | 2017-02-07 | ||
* | | | | | | | | | | | | | Extraction: remove the "print to devnull" hack now that pp isn't lazy anymore | 2017-02-07 | ||
* | | | | | | | | | | | | | Extraction: avoid deprecated functions of module String | 2017-02-07 | ||
* | | | | | | | | | | | | | Extraction: simplify the generated code for difficult name conflicts | 2017-02-07 | ||
* | | | | | | | | | | | | | Extraction : get_duplicates (via option) instead of check_duplicates (via Not... | 2017-02-07 | ||
* | | | | | | | | | | | | | configure: avoid deprecated warnings | 2017-02-07 | ||
* | | | | | | | | | | | | | Extraction: fix complexity issue #5310 | 2017-02-07 | ||
| | | | | * | | | | | | | | Extraction: fix complexity issue #5310 | 2017-02-07 | ||
| | | | | | * | | | | | | | Extraction: fix complexity issue #5310 | 2017-02-07 | ||
* | | | | | | | | | | | | | Merge PR#425: [travis] [External CI] [geocoq] don't build slow file | 2017-02-07 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | * | | | | | | Add test-suite files for hintdb variables in Ltac. | 2017-02-07 | ||
| | | | | | | | * | | | | | | Remove hackish autounfoldify now that hintdb can be bound to Ltac variables. | 2017-02-07 | ||
| | | | | | | | * | | | | | | pre_ident can be bound to Ltac variables. | 2017-02-07 | ||
| |_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | [travis] [External CI] [geocoq] don't build slow file | 2017-02-07 | ||
* | | | | | | | | | | | | | Merge PR#424: [travis] [External CI] iris-coq: fix dependencies | 2017-02-07 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ |