| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-20 | Improved chapter 'The tactic language' of the Reference Manual. | Zeimer | |
| 2018-07-20 | Also remove ClosedSection (same reasoning as ClosedModule) | Maxime Dénès | |
| 2018-07-20 | Remove ClosedModule from libstack | Maxime Dénès | |
| Seems unused and probably holds a lot of pointers. | |||
| 2018-07-20 | Added :undocumented: and :cmd: as suggested in comments for PR #8072. | Zeimer | |
| 2018-07-20 | Fixed many spelling and grammar errors in the chapters 'Vernacular ↵ | Zeimer | |
| commands', 'Proof handling' and 'Tactics' of the Reference Manual. Fixed some more serious errors related to tactics functional induction, unfold, hnf and red. Added some error messages and remarks for tactics btauto, rtauto and red. | |||
| 2018-07-20 | Fix #8043: Unsafe assignment in checker. | Pierre-Marie Pédrot | |
| We use a dedicated mutable constructor to perform a Landin knot. | |||
| 2018-07-20 | Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp. | Enrico Tassi | |
| 2018-07-20 | Merge PR #8089: Remove declare_object for SsrHave NoTCResolution. | Enrico Tassi | |
| 2018-07-20 | Merge PR #8070: Fixed some typos and grammar errors from section 'The ↵ | Théo Zimmermann | |
| language' of the Reference Manual. | |||
| 2018-07-19 | Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' ↵ | Zeimer | |
| of the Reference Manual. | |||
| 2018-07-19 | Fixed some typos and grammar errors from section 'The language' of the ↵ | Zeimer | |
| Reference Manual. Removed all mentions of prodT because it is no longer a separate inductive definition (prod has been living in Type for some time) but rather only a notation for prod needed for compatibility purposes. | |||
| 2018-07-19 | Merge PR #7941: Extend QuestionMark to produce a better error message in ↵ | Pierre-Marie Pédrot | |
| case of missing record field | |||
| 2018-07-19 | Remove declare_object for SsrHave NoTCResolution. | Maxime Dénès | |
| IIUC, this was a hack to make `Set SsrHave NoTCResolution` behave like `Global Set SsrHave NoTCResolution`. I don't think it is needed (just let the user write the desired locality), but if it is, the right way of doing it is to let clients of Goptions specify a default locality. | |||
| 2018-07-18 | Merge PR #8054: [dev] Autogenerate OCaml dev files. | Enrico Tassi | |
| 2018-07-18 | Merge PR #7897: Remove fourier plugin | Enrico Tassi | |
| 2018-07-18 | the same license as for the coq development | Yves Bertot | |
| 2018-07-18 | Merge PR #8068: [build] Build Coq and plugins with `-strict-sequence` | Enrico Tassi | |
| 2018-07-18 | Merge PR #8060: Remove useless libobject in proof_using | Enrico Tassi | |
| 2018-07-17 | Merge PR #8055: Fast accumulator check in native compilation | Maxime Dénès | |
| 2018-07-17 | Remove fourier plugin | Maxime Dénès | |
| As stated in the manual, the fourier tactic is subsumed by lra. | |||
| 2018-07-17 | change into QuestionMark default | Siddharth Bhat | |
| 2018-07-17 | Add overlay for Coq-Equations for QuestionMark. | Siddharth Bhat | |
| The changed QuestionMark structure breaks Coq-Equations. Add an overlay to fix this. | |||
| 2018-07-17 | Change QuestionMark for better record field missing error message. | Siddharth Bhat | |
| While we were adding a new field into `QuestionMark`, we decided to go ahead and refactor the constructor to hold an actual record. This record now holds the name, obligations, and whether the evar represents a missing record field. This is used to provide better error messages on missing record fields. | |||
| 2018-07-16 | Mention the automatic use of the rebase label. | Théo Zimmermann | |
| 2018-07-16 | Move long label links to the bottom of CONTRIBUTING.md | Théo Zimmermann | |
| 2018-07-16 | Restrict universes in comInductive | Jasper Hugunin | |
| Closes #7967. | |||
| 2018-07-16 | Merge PR #8069: Only check overlay extensions on git-tracked files | Gaëtan Gilbert | |
| 2018-07-16 | Add overlay for QuickChick | Jason Gross | |
| 2018-07-16 | Update CHANGES | Jason Gross | |
| 2018-07-16 | Add additional lemmas about {String,Ascii}.eqb | Jason Gross | |
| Lemma types and names coppied from [Search Z.eqb]. | |||
| 2018-07-16 | Add Extract Inlined Constant directives for {String,Ascii}.eqb | Jason Gross | |
| 2018-07-16 | Ascii.eqb and String.eqb | Pierre Letouzey | |
| 2018-07-16 | bin,oct,hex conversions positive,Z,N,nat<->string | Jason Gross | |
| 2018-07-16 | Only check overlay extensions on git-tracked files | Jason Gross | |
| This way, when editors leave over temporary files from editing user-overlays, we don't prevent commits unless they are added to git. | |||
| 2018-07-16 | Fix #7291: unify tactic should have more descriptive error messages. | Pierre-Marie Pédrot | |
| We simply reuse the same exception as the pretyper instead of raising the generic failure exception in Tactics.unify. | |||
| 2018-07-16 | Merge PR #8023: Introduce a team of code owners for the CI system. | Maxime Dénès | |
| 2018-07-16 | Merge PR #8066: [ltac] Remove unused functions. | Pierre-Marie Pédrot | |
| 2018-07-15 | Use GitHub as the location for OCaml sources. | Théo Zimmermann | |
| It will be more robust and more secure than downloading from the OCaml website. | |||
| 2018-07-14 | [build] Build Coq and plugins with `-strict-sequence` | Emilio Jesus Gallego Arias | |
| Fixes #8067. This is becoming the default in many developments, so it makes sense to require it too, both for Coq and for Plugins. | |||
| 2018-07-14 | [ltac] Remove unused functions / constructors. | Emilio Jesus Gallego Arias | |
| Catched by compiling the ml files from ml4. | |||
| 2018-07-13 | Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of ↵ | Théo Zimmermann | |
| the Reference Manual (Introduction, Credits). | |||
| 2018-07-13 | Remove useless libobject in proof_using | Maxime Dénès | |
| 2018-07-13 | Merge PR #6930: Make -warn-error fail on warnings emitted by coqc on stdlib. | Emilio Jesus Gallego Arias | |
| 2018-07-13 | Make -warn-error fail on warnings emitted by coqc on stdlib. | Maxime Dénès | |
| We turn all Coq warnings that are on by default into errors. | |||
| 2018-07-13 | Generate type-specific code for is_accu in native compilation of fixpoints. | Pierre-Marie Pédrot | |
| This is much more efficient than using Nativevalues.is_accu function which incurs a lot of irrelevant checks on its argument. | |||
| 2018-07-13 | Store the {struct} inductive type in native fixpoint AST. | Pierre-Marie Pédrot | |
| 2018-07-13 | Pass a proper environment to Nativelambda.lambda_of_constr. | Pierre-Marie Pédrot | |
| No need to roll up a new data structure when Environment has O(log n) add and lookup of rel definitions. | |||
| 2018-07-12 | Fixed typos, wording and grammar errors in the Preamble of the Reference ↵ | Zeimer | |
| Manual (Introduction, Credits). | |||
| 2018-07-12 | Merge PR #8041: [ci] Remove warning jobs in favor of default `-warn-error yes` | Gaëtan Gilbert | |
| 2018-07-12 | Merge PR #7907: Tactic deprecation machinery | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |