Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge PR#399: Debug by default | 2017-02-27 | |
|\ | |||
* \ | Merge PR#395: Allow hintdb to be parameters in a Ltac definition or | 2017-02-27 | |
|\ \ | |||
* | | | Revert "Add empty ltac_plugin file for forward compatibility." | 2017-02-24 | |
* | | | Fixing #use"include" after vernac is added and ltac is moved to a plugin. | 2017-02-23 | |
* | | | Merge branch 'v8.6' | 2017-02-22 | |
|\ \ \ | |||
| * \ \ | Merge branch 'v8.5' into v8.6 | 2017-02-22 | |
| |\ \ \ | |||
* | | | | | [travis] track an 8.7 specific branch of HoTT. | 2017-02-21 | |
* | | | | | Merge PR#309: Ltac as a plugin | 2017-02-21 | |
|\ \ \ \ \ | |||
| | * | | | | Add empty ltac_plugin file for forward compatibility. | 2017-02-21 | |
| | | | | * | Deprecate -debug flag. | 2017-02-20 | |
* | | | | | | Merge PR#189: Remove tabulation support from pretty-printing. | 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 | |
* | | | | | | 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 |