aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-01-08Update doc/changelog/02-specification-language/11368-trailing_implicit_error.rstSimonBoulier
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-01-08Trailing implicit: Maxime's suggestionsSimonBoulier
2020-01-07Merge PR #11245: [tools] Remove support for python2Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: vbgl
2020-01-07Merge PR #11369: [refman] Correct manual about implicit parameters in inductivesThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-07Correct manual about implicit parameters in inductives.SimonBoulier
2020-01-07Trailing implicit error: documentationSimonBoulier
2020-01-07Trailing implicit error: changelogSimonBoulier
2020-01-06doc: mention limitation of bidi hints vs programGaëtan Gilbert
No example as I'm not familiar enough with Program to make one.
2020-01-06[micromega] fix of bug #11191Frédéric Besson
- Add an instance to ZifyInst to instruct zify that 0 < x -> 0 < y -> 0 < Z.pow x y - More aggressive interval analysis to bound non-linear monomials.
2020-01-06Merge PR #11361: Fix #11360: discharge of template inductive with param only ↵Pierre-Marie Pédrot
use of var Reviewed-by: mattam82 Reviewed-by: ppedrot
2020-01-06Merge PR #11340: [refman] Fix bad quoting practice leftover from Sphinx ↵Clément Pit-Claudel
migration. Reviewed-by: jfehrle
2020-01-06stdlib List: add [remove'] and [count_occ']Yishuai Li
2020-01-06Fix #11360: discharge of template inductive with param only use of varGaëtan Gilbert
2020-01-03Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issueEnrico Tassi
Reviewed-by: gares
2020-01-03coq_makefile: don't use CAMLPKGS when building cmxa of mllibGaëtan Gilbert
It seems broken according to unicoq experiences https://gitter.im/coq/coq?at=5e0e3e0005298604982ac3f7 Building cmxa of mlpack is already this way.
2020-01-03[tools] Remove support for python2Emilio Jesus Gallego Arias
Closes #10491 We re-add the header in doc/tools/coqrst/notations/fontsupport.py which was removed by accident in 1a9c769ed363ee2f2784e7252af72e6c1e2fbcc6 The fontsupport script itself has been kept for reference, however it is not involved by any build target as of today.
2019-12-31Merge PR #11325: [refman] Add missing s.Pierre-Marie Pédrot
Reviewed-by: jfehrle
2019-12-30Merge PR #11233: Fixes #11231: missing dependency in looking for default ↵Pierre-Marie Pédrot
clauses in pattern matching decompilation algorithm Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-12-29Remove :flag: that appears in the outputJim Fehrle
2019-12-29[refman] Fix bad quoting practice leftover from Sphinx migration.Théo Zimmermann
2019-12-29Merge PR #11314: Convert productionlists in the Gallina chapter up to the ↵Théo Zimmermann
Vernacular section to prodns Reviewed-by: Zimmi48
2019-12-29Merge PR #11183: Enhance prodn in .rst doc files to support multiple ↵Théo Zimmermann
productions in a prodn Ack-by: Zimmi48 Ack-by: cpitclaudel
2019-12-28Prevent apostrophes and backticks from being stylized in latexJim Fehrle
2019-12-28Convert productionlists to prodnsJim Fehrle
2019-12-28Update doc/sphinx/language/gallina-extensions.rstKazuhiko Sakaguchi
Co-Authored-By: Cyril Cohen <CohenCyril@users.noreply.github.com>
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
The `Print Canonical Projections` command now can take constants and prints only the unification rules that involves or are synthesized from given constants.
2019-12-27docs: Update changes.rst w.r.t. ssrsetoid.v's simplificationErik Martin-Dorel
2019-12-26Add rew dependent NotationsJason Gross
This way when users `Import EqNotations`, we get pretty-printing for equality `match` statements too.
2019-12-26[omega] Remove non-documented "omega with *"Emilio Jesus Gallego Arias
This form is only used in coq-bignums and not documented. I think removal is the best choice, specially as `zify` is not part of the omega plugin anymore.
2019-12-26Deprecate the "omega with *" syntax.Pierre-Marie Pédrot
Changes to the test-suite were backported from PR #11288.
2019-12-25Show doc notations in boldfaceJim Fehrle
2019-12-24[Attributes] accept #[canonical] (Let|Definition)Enrico Tassi
2019-12-24[CS] Allow a variable introduced with Let to be a canonical instanceEnrico Tassi
2019-12-23Merge PR #11324: [refman] Mention Ltac2 in intro.Pierre-Marie Pédrot
Reviewed-by: jfehrle
2019-12-23Merge PR #10760: Make rapply handle all numbers of underscoresPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-12-22Apply suggestions from code reviewThéo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2019-12-22[refman] Mention Ltac2 in intro.Théo Zimmermann
2019-12-22[refman] Add missing s.Théo Zimmermann
2019-12-21Merge PR #11311: Fix handling of recursive notations with custom entriesHugo Herbelin
Reviewed-by: herbelin
2019-12-20Fix handling of recursive notations with custom entriesMaxime Dénès
Fixes #9532 Fixes #9490
2019-12-19Support additional escape sequences in notationsJim Fehrle
2019-12-20Coherence checking for coercionsKazuhiko Sakaguchi
This change improves the relaxed ambiguous path condition of coercions (#9743) to check that any circular inheritance path of `C >-> C` is definitionally equal to the identity function of the class `C`. Moreover, for a new inheritance path `p : C >-> D` and existing (valid) one `q : C >-> D`, the new mechanism does not report the ambiguity of `p` and `q` if they have a common element, that is to say: `p = p1 @ [c] @ p2` and `q = q1 @ [c] @ q2` for some coercion `c` and inheritance paths `p1`, `p2`, `q1`, and `q2`. In that case, convertibility of `p1` and `q1`, also, `p2` and `q2` should be checked; thus, checking the ambiguity of `p` and `q` is redundant with them. If the new mechanism does not report any ambiguous path, the inheritance graph must be coherent [Barthe 1995, Sect. 3.2] [Saïbi 1997, Sect. 7]: 1. for any circular path `p : C >-> C`, `p` is definitionally equal to the identity function, and 2. for any two paths `p, q : C >-> D`, `p` and `q` are convertible. [Barthe 1995] Gilles Barthe, Implicit coercions in type systems, In: TYPES '95, LNCS, vol 1158, Springer, 1996, pp 1-15. [Saïbi 1997] Amokrane Saïbi, Typing algorithm in type theory with inheritance, In: POPL '97, ACM, 1997, pp 292-301.
2019-12-18Merge PR #11203: Make the string argument of `time` print correctlyPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-12-18Merge PR #11263: [micromega] fix efficiency regressionMaxime Dénès
Reviewed-by: maximedenes
2019-12-17Merge PR #10762: Fix refine and eapply to mark shelved goals as ↵Maxime Dénès
non-resolvable, always Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-12-17[micromega] fix efficiency regressionFrédéric Besson
PR #9725 fixes completness bugs introduces some inefficiency. The current PR intends to fix the inefficiency while retaining completness. The fix removes a pre-processing step and instead relies on a more elaborate proof format introducing positivity constraints on the fly. Solve bootstrapping issues: RMicromega <-> Rbase <-> lia. Fixes #11063 and fixes #11242 and fixes #11270
2019-12-14Make prodn look more like productionlistJim Fehrle
2019-12-14Fix refine and eapply to mark shelved goals as non-resolvable, alwaysMatthieu Sozeau
Check that we don't regress on PR #10762 example Fix regression discovered by Arthur in PR #10762 Fix script of #10298 which was relying on breaking semantics for `eapply` Add doc Add comment in clenvtac Actually, always mark shelved goals as unresolvable Update doc to reflect semantics w.r.t. shelved subgoals
2019-12-13[doc] [INSTALL] Port INSTALL to markdown format.Emilio Jesus Gallego Arias
2019-12-12restrict minimization to set to flexiblesGaëtan Gilbert
Split from #10331 Fix part of #8196 Replaces #9343
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 03:15:05 +0000