aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
2018-08-13Do not run 32-bit Windows builds on pull requests.Théo Zimmermann
I have never seen this build fail without the 64-bit Windows build failing as well. So it is just a waste of time to test it on every pull request and we are short in Windows test machines.
2018-08-10one more fix to formulation of the Euclid Theorem in commentSamuel Gruetter
as pointed out by @jashug
2018-08-09fix formulation of the Euclid Theorem in commentSamuel Gruetter
2018-08-07fix three small typosLangston Barrett
2018-08-07doc/ltac2.md: add table of contentsLangston Barrett
2018-08-06Add regression test for issue #4202Tej Chajed
2018-08-06Merge PR #8189: Some trivial fixes to the custom entry documentation.Emilio Jesus Gallego Arias
2018-08-06Merge PR #8073: Use GitHub as the location for OCaml sources.Michael Soegtrop
2018-08-04Merge PR #8142: Improved the grammar and spelling of chapter 'Syntax ↵Théo Zimmermann
extensions and interpretation scopes' of the Reference Manual.
2018-08-04Improved the grammar and spelling of chapter 'Syntax extensions and ↵Zeimer
interpretation scopes' of the Reference Manual.
2018-08-04Merge PR #8216: Fix docs on arguments to setoid_replaceThéo Zimmermann
2018-08-03Fix docs on arguments to setoid_replace. Fixes #8213Langston Barrett
2018-08-02Merge PR #8143: Improved grammar and spelling in chapters 'Proof Schemes' ↵Théo Zimmermann
and 'The Coq commands' of the Reference Manual.
2018-08-02Merge PR #8145: Improved grammar and spelling in chapter 'Extended pattern ↵Théo Zimmermann
matching' of the Reference Manual.
2018-08-02Merge PR #8144: Improved grammar and spelling for chapters 'Utilities' and ↵Théo Zimmermann
'CoqIDE' of the Reference Manual.
2018-08-02Merge PR #8176: Improved grammar and spelling in chapters 'Type Classes', ↵Théo Zimmermann
'Omega' and 'Micromega' of the Reference Manual.
2018-08-02Merge PR #8185: Improved grammar and spelling in the remaining chapters of ↵Théo Zimmermann
the Reference Manual.
2018-08-01Fix broken link.Daniel R. Grayson
2018-08-01Added a tactic index entry for nsatz, reformatted commands in chapter ↵Zeimer
'Generalized Rewriting' and renamed the chapter Nsatz from _nsatz to _nsatz_chapter.
2018-08-01Improved grammar and spelling in the remaining chapters of the Reference Manual.Zeimer
2018-08-01Improved grammar and spelling in chapter 'Extended pattern matching' of the ↵Zeimer
Reference Manual.
2018-08-01Improved grammar and spelling in chapters 'Proof Schemes' and 'The Coq ↵Zeimer
commands' of the Reference Manual.
2018-08-01Improved grammar and spelling in chapters 'Type Classes', 'Omega' and ↵Zeimer
'Micromega' of the Reference Manual.
2018-08-01Merge PR #8169: NArith: add sized N2BvHugo Herbelin
2018-08-01Update documentation on GitLab CI to reflect recent changes.Théo Zimmermann
2018-08-01Improved grammar and spelling for chapters 'Utilities' and 'CoqIDE' of the ↵Zeimer
Reference Manual.
2018-08-01Merge PR #8151: Vector: expose ++ to userHugo Herbelin
2018-08-01Merge PR #8182: Handle diffs better for the "Undo" command.Enrico Tassi
2018-08-01Merge PR #8192: Fix typos and typesetting of doc on ProgramThéo Zimmermann
2018-08-01Merge PR #8184: Improved grammar and spelling in chapters 'Extraction', ↵Théo Zimmermann
'Program' and 'ring and field' chapters of the Reference Manual.
2018-08-01Merge PR #8191: [sphinx] Use arguments of '.. example::' directive as a titleThéo Zimmermann
2018-08-01Merge PR #8195: Fix doc for no associativityThéo Zimmermann
2018-07-31Camlp{4 => 5}Jason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 22:59:58 +0000