| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| * | | | | | | | Merge PR#395: Allow hintdb to be parameters in a Ltac definition or |  Maxime Dénès | 2017-02-27 | |
| |\ \ \ \ \ \ \ | ||||
| | | | | | * | | | [travis] [External CI] fiat-parsers |  Emilio Jesus Gallego Arias | 2017-02-24 | |
| | | | | |/ / / | ||||
| * | | | / / / | Revert "Add empty ltac_plugin file for forward compatibility." | Maxime Dénès | 2017-02-24 | |
| | |_|_|/ / / |/| | | | | | ||||
| * | | | | | | Fixing #use"include" after vernac is added and ltac is moved to a plugin. |  Hugo Herbelin | 2017-02-23 | |
| * | | | | | | Merge branch 'v8.6' |  Pierre-Marie Pédrot | 2017-02-22 | |
| |\ \ \ \ \ \ | ||||
| | * \ \ \ \ \ | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2017-02-22 | |
| | |\ \ \ \ \ \ | ||||
| * | | | | | | | | [travis] track an 8.7 specific branch of HoTT. | Maxime Dénès | 2017-02-21 | |
| * | | | | | | | | Merge PR#309: Ltac as a plugin | Maxime Dénès | 2017-02-21 | |
| |\ \ \ \ \ \ \ \ | ||||
| | | * | | | | | | | Add empty ltac_plugin file for forward compatibility. | Maxime Dénès | 2017-02-21 | |
| | | | | | * | | | | Deprecate -debug flag. | Maxime Dénès | 2017-02-20 | |
| * | | | | | | | | | Merge PR#189: Remove tabulation support from pretty-printing. | Maxime Dénès | 2017-02-20 | |
| |\ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | * \ | Merge pull request #4 from Zimmi48/patch-1 | Emilio Jesús Gallego Arias | 2017-02-20 | |
| | | | | | | | | |\ \ | ||||
| | | | | | | | | | * | | [ocamlbuild] fix small mistakes in descriptions |  Théo Zimmermann | 2017-02-20 | |
| | | | | | | | | |/ / | ||||
| | | | | | | | | * | | [ocamlbuild] Update meta for the vernac split. | Emilio Jesus Gallego Arias | 2017-02-20 | |
| * | | | | | | | | | | Fixing debugger after the split of toplevel into vernac. | Pierre-Marie Pédrot | 2017-02-19 | |
| | |_|_|_|_|_|_|/ / |/| | | | | | | | | ||||
| * | | | | | | | | | remove obsolete file dev/Makefile.oug |  Pierre Letouzey | 2017-02-17 | |
| | | * | | | | | | | Removing spurious folder includes in coq_makefile. | Pierre-Marie Pédrot | 2017-02-17 | |
| | | * | | | | | | | Documenting the pluginification of Ltac. | Pierre-Marie Pédrot | 2017-02-17 | |
| | | * | | | | | | | Fix .gitignore. | Pierre-Marie Pédrot | 2017-02-17 | |
| | | * | | | | | | | Moving the Ltac plugin to a pack-based one. | Pierre-Marie Pédrot | 2017-02-17 | |
| | | * | | | | | | | Ltac as a plugin. | Pierre-Marie Pédrot | 2017-02-17 | |
| | |/ / / / / / / |/| | | | | | | | ||||
| | | * | | | | | | Fixing #5339 (anomaly with 'pat in record parameters). | Hugo Herbelin | 2017-02-16 | |
| | | | | | | | * | [cleanup] Change Id.t option to Name.t in TacFun |  Tej Chajed | 2017-02-16 | |
| | |_|_|_|_|_|/ |/| | | | | | | ||||
| * | | | | | | | Merge PR#403: Split Vernacular Processing from Toplevel | Maxime Dénès | 2017-02-16 | |
| |\ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ | Merge PR#431 | Maxime Dénès | 2017-02-16 | |
| |\ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | [travis] [External CI] CompCert official 8.6 support + UniMath | Emilio Jesus Gallego Arias | 2017-02-15 | |
| | * | | | | | | | | [travis] [External CI] Factor out math-comp installs. | Emilio Jesus Gallego Arias | 2017-02-15 | |
| | | * | | | | | | | Make Obligations see fix_exn |  Enrico Tassi | 2017-02-15 | |
| | | * | | | | | | | [stm] Remove unused legacy stm interface. | Emilio Jesus Gallego Arias | 2017-02-15 | |
| | | * | | | | | | | [cosmetic] Reorder makefile as suggested by @herbelin | Emilio Jesus Gallego Arias | 2017-02-15 | |
| | | * | | | | | | | [stm] Reenable Show Script command. | Emilio Jesus Gallego Arias | 2017-02-15 | |
| | | * | | | | | | | [stm] Break stm/toplevel dependency loop. | Emilio Jesus Gallego Arias | 2017-02-15 | |
| | |/ / / / / / / |/| | | | | | | | ||||
| * | | | | | | | | Merge PR#314: Miscellaneous fixes for Ocaml warnings. | Maxime Dénès | 2017-02-15 | |
| |\| | | | | | | | ||||
| | * | | | | | | | [unicode] Address comments in PR#314. | Emilio Jesus Gallego Arias | 2017-02-15 | |
| | * | | | | | | | [safe-string] Switch to buffer to `Bytes` | Emilio Jesus Gallego Arias | 2017-02-14 | |
| | * | | | | | | | [safe-string] Use `String.init` to build string. | Emilio Jesus Gallego Arias | 2017-02-14 | |
| | * | | | | | | | [misc] Remove unused binding. | Emilio Jesus Gallego Arias | 2017-02-14 | |
| |/ / / / / / / | ||||
| * | | | | | | | Merge PR#253: Sort Search results by relevance | Maxime Dénès | 2017-02-14 | |
| |\ \ \ \ \ \ \ | ||||
| | * | | | | | | | Test-suite: output of Search |  Arnaud Spiwack | 2017-02-14 | |
| * | | | | | | | | Merge PR#349: Proofview: tclINDEPENDENTL | Maxime Dénès | 2017-02-13 | |
| |\ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | Proofview: tclINDEPENDENTL | Enrico Tassi | 2017-02-10 | |
| |/ / / / / / / / | ||||
| | | | * | | | | | Turning an anomaly on 'pat into a proper "unsupported" error message. | Hugo Herbelin | 2017-02-09 | |
| | | | * | | | | | Fixing bug #5346 (an unimplemented application of 'pat). | Hugo Herbelin | 2017-02-09 | |
| * | | | | | | | | Merge PR#405: Type cleanup in `Metasyntax` | Maxime Dénès | 2017-02-08 | |
| |\ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ | Merge PR#393: Replace Typeops with Fast_typeops | Maxime Dénès | 2017-02-08 | |
| |\ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | Revert "Extraction: avoid deprecated functions of module String" | Pierre Letouzey | 2017-02-07 | |
| * | | | | | | | | | | Extraction cosmetic: no whitespaces in printing empty modules | Pierre Letouzey | 2017-02-07 | |
| * | | | | | | | | | | Extraction: remove the "print to devnull" hack now that pp isn't lazy anymore | Pierre Letouzey | 2017-02-07 | |
| * | | | | | | | | | | Extraction: avoid deprecated functions of module String | Pierre Letouzey | 2017-02-07 | |
| * | | | | | | | | | | Extraction: simplify the generated code for difficult name conflicts | Pierre Letouzey | 2017-02-07 | |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |