aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-23Generate more compact escape sequences byJim
a) not explicitly setting the default value and b) not repeating attributes that are already set. Example (omitting escape character): Old: E : [92;49;22;23;24;27mev[39;49;22;23;24;27m [39;49;22;23;24;27mn[39;49;22;23;24;27m New: E : [92mev[0m n (92 is bright green, the other codes set default attributes).
2018-07-23Adding environment-manipulating functions.Pierre-Marie Pédrot
2018-07-23Fix deprecated warnings from Pcoq.Pierre-Marie Pédrot
2018-07-23Merge remote-tracking branch 'origin/pr/54'Pierre-Marie Pédrot
2018-07-22Merge PR #8095: Improvements for the chapter 'Detailed examples of tactics' ↵Théo Zimmermann
of the Reference Manual.
2018-07-22Docs: minor typo in "Template Polymorphism"Timothy Bourke
2018-07-22Docs: minor typo in W-Ind relative to textTimothy Bourke
The rule uses s'_j, the text refers to s_j, the latter is simpler in the absence of any other constraints.
2018-07-21Solved problems with snippets giving errors in chapter 'Detailed examples of ↵Zeimer
tactics' of the Reference Manual. Refreshed the section on the cardinality of the naturals. Removed the mention of specialize_eqs as it seems very bugged.
2018-07-21Rewrote examples about permutations, logic and type isomorphisms: changed ↵Zeimer
the formatting and renamed the tactics to match modern naming conventions.
2018-07-21Improvements for the chapter 'Detailed examples of tactics' of the Reference ↵Zeimer
Manual.
2018-07-21Docs: Fix p values in CIC Inductive Defs examplesTimothy Bourke
It seems that p is a natural number, so why not write it as 0 rather than the empty list for tree and forest? And, if I understand correctly, odd and even have p = 0 and Arr(even) = Arr(odd) = 1.
2018-07-21Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' ↵Théo Zimmermann
and 'Tactics' of the Reference Manual.
2018-07-21Fixing capital letters in the "in" syntax of instantiate.Hugo Herbelin
This trace of V7 syntax remained unnoticed (since July 2004).
2018-07-21[doc] Fix grammar of goal selectors.Théo Zimmermann
2018-07-21A few Sphinx fixes in the Ltac chapter.Théo Zimmermann
Including using subscripts more often.
2018-07-21Merge PR #8086: Improved chapter 'The tactic language' of the Reference Manual.Théo Zimmermann
2018-07-20Small improvements suggested in comments to PR #8086.Zeimer
2018-07-20Improved chapter 'The tactic language' of the Reference Manual.Zeimer
2018-07-20Also remove ClosedSection (same reasoning as ClosedModule)Maxime Dénès
2018-07-20Remove ClosedModule from libstackMaxime Dénès
Seems unused and probably holds a lot of pointers.
2018-07-20Added :undocumented: and :cmd: as suggested in comments for PR #8072.Zeimer
2018-07-20Fixed 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-20Fix #8043: Unsafe assignment in checker.Pierre-Marie Pédrot
We use a dedicated mutable constructor to perform a Landin knot.
2018-07-20Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp.Enrico Tassi
2018-07-20Merge PR #8089: Remove declare_object for SsrHave NoTCResolution.Enrico Tassi
2018-07-20Merge PR #8070: Fixed some typos and grammar errors from section 'The ↵Théo Zimmermann
language' of the Reference Manual.
2018-07-19Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' ↵Zeimer
of the Reference Manual.
2018-07-19Fixed 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-19Merge PR #7941: Extend QuestionMark to produce a better error message in ↵Pierre-Marie Pédrot
case of missing record field
2018-07-19Remove 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-18Merge PR #8054: [dev] Autogenerate OCaml dev files.Enrico Tassi
2018-07-18Merge PR #7897: Remove fourier pluginEnrico Tassi
2018-07-18the same license as for the coq developmentYves Bertot
2018-07-18Merge PR #8068: [build] Build Coq and plugins with `-strict-sequence`Enrico Tassi
2018-07-18Merge PR #8060: Remove useless libobject in proof_usingEnrico Tassi
2018-07-17Merge PR #8055: Fast accumulator check in native compilationMaxime Dénès
2018-07-17Remove fourier pluginMaxime Dénès
As stated in the manual, the fourier tactic is subsumed by lra.
2018-07-17change into QuestionMark defaultSiddharth Bhat
2018-07-17Add overlay for Coq-Equations for QuestionMark.Siddharth Bhat
The changed QuestionMark structure breaks Coq-Equations. Add an overlay to fix this.
2018-07-17Change 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-16Mention the automatic use of the rebase label.Théo Zimmermann
2018-07-16Move long label links to the bottom of CONTRIBUTING.mdThéo Zimmermann
2018-07-16Restrict universes in comInductiveJasper Hugunin
Closes #7967.
2018-07-16Merge PR #8069: Only check overlay extensions on git-tracked filesGaëtan Gilbert
2018-07-16Add overlay for QuickChickJason Gross
2018-07-16Update CHANGESJason Gross
2018-07-16Add additional lemmas about {String,Ascii}.eqbJason Gross
Lemma types and names coppied from [Search Z.eqb].
2018-07-16Add Extract Inlined Constant directives for {String,Ascii}.eqbJason Gross
2018-07-16Ascii.eqb and String.eqbPierre Letouzey
2018-07-16bin,oct,hex conversions positive,Z,N,nat<->stringJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 06:48:50 +0000