aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-08-28Fix #8288: cumulativity inferance ignores args to bound variablesGaëtan Gilbert
(NB: only variables whose binder is inside the constructor argument, ie Inductive foo := C : forall A : Type -> Type, A Type -> foo. does not trigger the bug because A becomes a RelKey.)
2018-08-28Fix #7795: UGraph.AlreadyDeclared with ProgramGaëtan Gilbert
This change is based on noticing that we use a default value for the `sideff` argument even though we have a similarly named `side_eff` available. Someone who knows how side effects and universes are supposed to interact should check this.
2018-08-28Merge PR #8112: Add support for focusing on named goals using brackets.Pierre-Marie Pédrot
2018-08-27Update test-suite for focusing on named goals.Théo Zimmermann
2018-08-27Document focusing on named goals.Théo Zimmermann
2018-08-27Add support for focusing on named goals using brackets.Théo Zimmermann
2018-08-27Merge PR #8312: Split up fiat-crypto CI into two targetsGaëtan Gilbert
2018-08-27Merge PR #8260: Tweak diff options in CoqIDEPierre-Marie Pédrot
2018-08-27Fix a casing problem noticed by Lars Dölle on Coq-Club.Théo Zimmermann
2018-08-27Merge PR #8293: Fix typo of caracterisation -> c*h*aracterisationHugo Herbelin
2018-08-27Fix wwwrefman and wwwstdlibKazuhiko Sakaguchi
2018-08-24Bug fix: restore previous printing behavior that was unintentionally changed ↵Jim Fehrle
in 7d2a9df (current code always prints context, should print only if the proof has changed). Bug fix: Fix message that came out as "Error: Error: -diffs requires ..." Enhancement: always print the context after the "Set Diffs" command.
2018-08-24Merge PR #8266: Minor Sphinx improvements in the bullet documentation.Clément Pit-Claudel
2018-08-24Fix ordering of before/after in print-pretty-timed-*Jason Gross
Fixes #8158
2018-08-24Split up fiat-crypto CI into two targetsJason Gross
There is the new pipeline, and the old pipeline. Most of what they share in common is the (very large) library of lemmas about `Z`. As per the discussion in https://github.com/coq/coq/pull/8064#issuecomment-413474176 through https://github.com/coq/coq/pull/8064#issuecomment-413793143
2018-08-23Merge PR #8296: Fix #8251: remove "the the" occurrencesThéo Zimmermann
2018-08-23Merge PR #8300: Fix issue #8298 OCaml 4.07 download path is incorrectThéo Zimmermann
2018-08-22Fix issue #8298 OCaml 4.07 download path is incorrectMichael Soegtrop
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-08-22Fix typo of caracterisation -> c*h*aracterisationSiddharth Bhat
2018-08-22Add missing spaces.Théo Zimmermann
2018-08-22[sphinx] Improve Case analysis and induction section.Théo Zimmermann
2018-08-22[refman] Fixing two nested lemma errors.Théo Zimmermann
2018-08-22[sphinx] Fixing of the beginning of the Tactics chapter.Théo Zimmermann
2018-08-21Merge PR #8249: Remove unneeded file stm/workerLoop.mliEnrico Tassi
2018-08-21[coq_makefile] print all options (Fix #7529)Enrico Tassi
2018-08-21Trivial Sphinx fix in doc.Théo Zimmermann
2018-08-20Merge PR #8258: Update documentation on GitLab CI to reflect recent changes.Emilio Jesus Gallego Arias
2018-08-20Merge PR #8136: Do not run 32-bit Windows builds on pull requests.Emilio Jesus Gallego Arias
2018-08-20Merge PR #8262: Remove dead argument allow_old.Emilio Jesus Gallego Arias
2018-08-20Do not inline let-bound functions in clambda optimization.Pierre-Marie Pédrot
This was triggering an exponential blowup in the size of the generated intermediate VM code. Fixes #8277.
2018-08-18Merge PR #8272: Fix typo in documentation, heigth --> height.Théo Zimmermann
2018-08-17Fix typo in documentation, heigth --> height.Nick Lewycky
2018-08-17Define bullet production token.Théo Zimmermann
2018-08-17Minor Sphinx improvements in the bullet documentation.Théo Zimmermann
And fixing a problem with nested proofs.
2018-08-17More efficient computation of avoided variables during pretyping.Pierre-Marie Pédrot
2018-08-17Do not abstract over the named variable in unsafe introduction tactic.Pierre-Marie Pédrot
There is no point in doing that. The term being abstracted does not contain the named variable y, as it is an evar of the form ?e{Var x_1, ... Var x_n, Rel 1}. In practice it means that only the binding creation matters, the substitution behaving as the identity, and ending up costing for nothing.
2018-08-17Remove dead argument allow_old.Théo Zimmermann
2018-08-161) Make the diff setting a persistent settting.Jim Fehrle
2) Changing the diff setting from the menu should reprint the proof. 3) Generate a warning message if the user enters a "Set Diffs xx" command. 4) Tweak display names for diffs in View menu.
2018-08-16Merge PR #8250: Introduce a team of code owners for the documentation.Maxime Dénès
2018-08-16Merge PR #8198: Fix broken link.Maxime Dénès
2018-08-16Merge PR #8111: Docs: Fix p values in CIC Inductive Defs examplesMaxime Dénès
2018-08-16Merge PR #8109: [doc] Fix grammar of goal selectors.Maxime Dénès
2018-08-16Merge PR #8108: A few Sphinx fixes in the Ltac chapter.Maxime Dénès
2018-08-16Merge PR #8079: Document the automatic use of the rebase label.Maxime Dénès
2018-08-15tacmach: function to gather undef evars of the goalMatthieu Sozeau
2018-08-14Merge PR #8221: Add regression test for issue #4202Théo Zimmermann
2018-08-14Introduce a team of code owners for the documentation.Théo Zimmermann
As was previously done for the CI, this means that there are no more principal / secondary code owners. All the member of the team can choose to review and self-assign any documentation PR that is not their own.
2018-08-14Remove unneeded file: workerLoop.ml/.mli were moved to toplevel in commit ↵Jim Fehrle
382ee49 but stm/workerLoop.mli was not removed as it should have been. Hasta la vista.
2018-08-13Less crazy implementation of the "pose" family of tactics.Pierre-Marie Pédrot
The previous implementation was calling a lot of useless unification even though the net effect of the tactic was simply to add a binding to the environment. Interestingly the base tactic was used in several higher level tactics, including evar and ssreflect pose. Part of the fix for #8245.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-04 13:00:55 +0000