| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-30 | Better support for make TIMED=1 on Windows | Jason Gross | |
| This fixes [bug #5619](https://coq.inria.fr/bugs/show_bug.cgi?id=5619) | |||
| 2017-06-30 | Merge PR#846: Fix OS X Travis by pinning OCaml version. | Maxime Dénès | |
| 2017-06-30 | Merge PR#843: closing bug #5618 introduce by PR 828 | Maxime Dénès | |
| 2017-06-30 | Mention again how to report bug and get version number. | Théo Zimmermann | |
| As suggested by @psteckler. | |||
| 2017-06-30 | Fix OS X Travis by pinning OCaml version. | Théo Zimmermann | |
| 2017-06-29 | Fix Zmod_div. | Russell O'Connor | |
| 2017-06-29 | Use forall for consistency | roconnor-blockstream | |
| 2017-06-29 | Add Z.mod_div lemma to standard library. | Russell O'Connor | |
| 2017-06-29 | Better phrasing. | Théo Zimmermann | |
| 2017-06-29 | More substance on discouraged practices. | Théo Zimmermann | |
| 2017-06-29 | closing bug #5618 introduce by PR 828 | Julien Forest | |
| 2017-06-29 | Some more corrections to the tutorial. | Théo Zimmermann | |
| 2017-06-29 | Mask the reliance on coqtop. | Théo Zimmermann | |
| 2017-06-29 | [meta] [api] Fix META file for API introduction. | Emilio Jesus Gallego Arias | |
| 2017-06-28 | Update the Tutorial. | Théo Zimmermann | |
| 2017-06-28 | A fix for #5598 (no discharge of Existing Classes referring to local variables). | Hugo Herbelin | |
| 2017-06-28 | Avoiding an optional int rather than using -1 to encode a local flag. | Hugo Herbelin | |
| Also giving the proper local flag to the hint registration, even on a Global instance, since the instance discharge manage itself the redefinition of a hint. | |||
| 2017-06-27 | Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails ↵ | Maxime Dénès | |
| with make -j4 | |||
| 2017-06-27 | Merge PR#731: Mini-cleaning around OCaml file names | Maxime Dénès | |
| This is only a partial merge, we stick with using the standard OCaml (un)capitalize functions. | |||
| 2017-06-27 | A cleaning phase about ocaml file names. | Hugo Herbelin | |
| Ocaml file names are restricted since 2008 to A..Z followed by a..z0..9'_. We take this constraint into account in tools manipulating Ocaml file names. | |||
| 2017-06-27 | Preparing to hints supporting discharge. | Hugo Herbelin | |
| I.e., do not set local flag to false when in a section since compatibility tells discharge of hints is not supported. | |||
| 2017-06-27 | Merge PR#814: Fix #5380: Default colors for CoqIDE are actually applied. | Maxime Dénès | |
| 2017-06-26 | Merge PR#826: Put plugin exports in the right compatibility file | Maxime Dénès | |
| 2017-06-26 | disable async on Windows by default | Paul Steckler | |
| 2017-06-26 | Merge PR#825: Ignore all PDF files. | Maxime Dénès | |
| 2017-06-26 | Merge PR#828: closing bug #4250 | Maxime Dénès | |
| 2017-06-26 | Bump version number to 8.6.1. | Maxime Dénès | |
| 2017-06-26 | Fix libpcre dependency issue under Windows. | Maxime Dénès | |
| 2017-06-26 | Fix proxy setting issue | Michael Soegtrop | |
| 2017-06-26 | Fixes bug #5561,#5562 in Windows build system | Michael Soegtrop | |
| 2017-06-26 | Merge PR#756: Fix Bug #5574, document function scope | Maxime Dénès | |
| 2017-06-25 | Reorganizing functions to find the relative position of an hypothesis. | Hugo Herbelin | |
| Also fixing a bug of get_next_hyp_position when the hypothesis is the oldest of the context (see test in ltac.v). | |||
| 2017-06-25 | Moving "assert" (internally "Cut") to the new proof engine. | Hugo Herbelin | |
| It allows in particular to have "Info" on tactic "assert" and derivatives not to give an "<unknown>". | |||
| 2017-06-25 | Exporting general-purpose functions on goal contexts from "logic.ml" to ↵ | Hugo Herbelin | |
| "tactics.ml". This is in preparation of move of "assert" from old to new proof engine. | |||
| 2017-06-25 | Adding intermediate entry point to create an evar in empty rel_context. | Hugo Herbelin | |
| 2017-06-23 | Merge PR#824: Fix printers | Maxime Dénès | |
| 2017-06-23 | Merge PR#821: [vernac] Remove stale bool parameter from ↵ | Maxime Dénès | |
| `VernacStartTheoremProof` | |||
| 2017-06-23 | Merge PR#820: [ide] Correct more merging errors. | Maxime Dénès | |
| 2017-06-23 | Merge PR#815: STM: par: report no error to UIs in non-solve mode | Maxime Dénès | |
| 2017-06-23 | Merge PR#794: Cleanup of ltac cmxs | Maxime Dénès | |
| 2017-06-23 | Merge PR#762: [vernac] Fix unneeded mutual references in Obligations | Maxime Dénès | |
| 2017-06-23 | Merge PR#813: Fix plugin warnings | Maxime Dénès | |
| 2017-06-23 | Fix Bug #5574, document function scope | Paul Steckler | |
| 2017-06-23 | closing bug #4250 | Julien Forest | |
| 2017-06-23 | [configure] 'ocaml' is more precise than OCaml as we mean the binary. | Maxime Dénès | |
| Fix suggested by Hugo. | |||
| 2017-06-23 | ocaml -> OCaml in configure.ml. | Maxime Dénès | |
| 2017-06-23 | Merge PR#729: Fixing an inconsistency between configure and configure.ml | Maxime Dénès | |
| 2017-06-23 | Merge PR#740: Refactor documentation of records. | Maxime Dénès | |
| 2017-06-23 | Add tests for handling of warnings | Tej Chajed | |
| 2017-06-23 | Fix bug 5392: Warnings defined in plugins are considered unknown | Maxime Dénès | |
| The status of a warning can now be set before the warning is declared (typically by a plugin). However, I had to remove the "unknown warning" warning. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |