| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-03-03 | Logic library: Adding a characterization of excluded-middle in term of | Hugo Herbelin | |
| choice of a representative in a partition of bool. Also move a result about propositional extensionality from ClassicalFacts.v to PropExtensionalityFacts.v, generalizing it by symmetry. Also spotting typos (thanks to Théo). | |||
| 2017-03-03 | Formatting references with surrounding brackets in Diaconescu.v. | Hugo Herbelin | |
| 2017-02-27 | Merge PR#399: Debug by default | Maxime Dénès | |
| 2017-02-27 | Merge PR#395: Allow hintdb to be parameters in a Ltac definition or | Maxime Dénès | |
| Tactic Notation | |||
| 2017-02-24 | Revert "Add empty ltac_plugin file for forward compatibility." | Maxime Dénès | |
| This reverts commit e8137ae63b3b19436755f372b595e7343e942894, was meant for 8.6 branch only. | |||
| 2017-02-23 | Fixing #use"include" after vernac is added and ltac is moved to a plugin. | Hugo Herbelin | |
| 2017-02-22 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-02-22 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2017-02-21 | [travis] track an 8.7 specific branch of HoTT. | Maxime Dénès | |
| This is required since we merged PR#309: Ltac as a plugin. | |||
| 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 | |
| This is in preparation for landing of PR#309: Ltac as a plugin | |||
| 2017-02-20 | 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-19 | Fixing debugger after the split of toplevel into vernac. | Pierre-Marie Pédrot | |
| 2017-02-17 | 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 | |
| This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements. | |||
| 2017-02-17 | Ltac as a plugin. | Pierre-Marie Pédrot | |
| This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin. | |||
| 2017-02-16 | Fixing #5339 (anomaly with 'pat in record parameters). | Hugo Herbelin | |
| 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 | |
| [travis] Add math-comp overlays, update CompCert to official version, add UniMath | |||
| 2017-02-15 | [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 | |
| We make math-comp overlays easier, we also start structuring the scripts a bit more. | |||
| 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 | |
| We extend `Stm.vernac_interp` so it can handle the commands it should by level. This reenables `Show Script` handling, and this interpretation function should handle more commands in the future such as Load. However note that we must first refactor the parsing state handling a bit and remove the legacy `Stm.interp` before that. | |||
| 2017-02-15 | [stm] Break stm/toplevel dependency loop. | Emilio Jesus Gallego Arias | |
| Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore. | |||
| 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-14 | [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 | |
| Fix the ordering of the results in the output of Search to correspond to the "priority" ordering. | |||
| 2017-02-13 | Merge PR#349: Proofview: tclINDEPENDENTL | Maxime Dénès | |
| 2017-02-10 | Proofview: tclINDEPENDENTL | Enrico Tassi | |
| 2017-02-09 | 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-08 | 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-07 | Revert "Extraction: avoid deprecated functions of module String" | Pierre Letouzey | |
| This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263. String.capitalize_ascii are only available for ocaml >= 4.03, sorry... | |||
| 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 | |
| - A few tweaks of string are now done via the Bytes module - lots of String.capitalize_ascii and co | |||
| 2017-02-07 | Extraction: simplify the generated code for difficult name conflicts | Pierre Letouzey | |
| No more pp_alias_spec et pp_alias_decl. Instead, we use "include" and "module type of". The extracted code might hence need OCaml 3.12 (quite rarely) | |||
| 2017-02-07 | Extraction : get_duplicates (via option) instead of check_duplicates (via ↵ | Pierre Letouzey | |
| Not_found) This clarifies the execution flow | |||
| 2017-02-07 | configure: avoid deprecated warnings | Pierre Letouzey | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |