aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-05-07Improve field_simplify on fractions with constant denominatorthery
Before this patch, `x` was "simplified" to `x / 1`.
2019-05-07Merge PR #10077: [refman] Add a note reminding about the typeclass_instances ↵Clément Pit-Claudel
database. Reviewed-by: cpitclaudel
2019-05-07Merge PR #10016: [test-suite] Remove a test with a Timeout that fails ↵Vincent Laporte
frequently on CI. Reviewed-by: vbgl
2019-05-07Merge PR #10053: Document change_no_check variantsThéo Zimmermann
Ack-by: JasonGross Reviewed-by: Zimmi48
2019-05-07Merge PR #10075: [Record] Une a record to gather field declaration attributesEnrico Tassi
Reviewed-by: gares
2019-05-07Merge PR #10002: Integrate ltac2Théo Zimmermann
Ack-by: JasonGross Reviewed-by: gares Reviewed-by: ppedrot Reviewed-by: jfehrle Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-05-07[refman] Add a note reminding about the typeclass_instances database.Théo Zimmermann
Closes #10072.
2019-05-07Merge PR #10063: CoqIDE: recognize qualified identifiers as words.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-05-07[Record] Une a record to gather field declaration attributesVincent Laporte
2019-05-07[Record] DeforestationVincent Laporte
2019-05-07[Canonical structures] DeforestationVincent Laporte
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
Since Ltac2 cannot be put under the stdlib logical root (some file names would clash), we move it to the `user-contrib` directory, to avoid adding another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego. Thanks to @Zimmi48 for the thorough documentation review and the numerous suggestions.
2019-05-06Merge PR #10068: Coqchk: encapsulating an anomaly NotConvertible into a ↵Pierre-Marie Pédrot
proper user-level typing error Reviewed-by: ppedrot
2019-05-06Merge PR #9964: Unreleased changelog folderVincent Laporte
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Reviewed-by: vbgl
2019-05-06Coqchk: encapsulating an anomaly NotConvertible into a proper typing error.Hugo Herbelin
Detected incidentally in "validate" check for #8893.
2019-05-05Add changelog entry about moving changelog to refman.Théo Zimmermann
2019-05-05[make] build unreleased.rstEnrico Tassi
2019-05-05Create categories in changelog.Théo Zimmermann
2019-05-05New infrastructure for the unreleased changelog.Théo Zimmermann
Move existing entries.
2019-05-05Merge PR #10059: Fixing bugs introduced in change_no_checkPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-05-04Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars.Pierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot
2019-05-04Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that appear ↵Pierre-Marie Pédrot
as assumptions Ack-by: RalfJung Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: maximedenes Reviewed-by: ppedrot Ack-by: robbertkrebbers
2019-05-04Merge PR #10012: Document convert_concl_no_check (#3225)Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48
2019-05-04Merge PR #10057: Fix #10054: Numeral Notations without the ltac plugin.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-05-03CoqIDE: recognize qualified identifiers as words.Jasper Hugunin
Fixes coq/coq#10062. The implementation is rough, and does not deal with leading, trailing, or doubled periods, but the same can be said of the current handling of leading numbers or primes.
2019-05-03Tactics: fixing "change_no_check in".Hugo Herbelin
(Merge of the initial version with #9983 was broken)
2019-05-03Updating CHANGES.Hugo Herbelin
2019-05-03Merge PR #9984: Add PairUsualDecidableTypeFullThéo Zimmermann
Reviewed-by: herbelin
2019-05-03Merge PR #10025: Fix #9994: `revert dependent` is extremely slow.Vincent Laporte
Ack-by: ppedrot Reviewed-by: vbgl
2019-05-03Fix #9994: `revert dependent` is extremely slow.Pierre-Marie Pédrot
We add a fast path when generalizing over variables.
2019-05-03Fix #10054: Numeral Notations without the ltac plugin.Pierre-Marie Pédrot
It was fairly easy, the plugin defined an argument that was only used in a vernacular extension. Thus marking it as VERNAC was enough not to link to Ltac.
2019-05-03Copy-editing from code reviewJason Gross
Co-Authored-By: Blaisorblade <p.giarrusso@gmail.com>
2019-05-03Documentation for change_no_check untested variantsPaolo G. Giarrusso
Copy change's variants in change_no_check, since supposedly they should all be supported. But they haven't been tested, and my example fails.
2019-05-03Document _no_check tactics (#3225)Paolo G. Giarrusso
Triggered by trying to understand https://gitlab.mpi-sws.org/iris/iris/merge_requests/235. - Add a new section at the end - Document change_no_check, and convert_concl_no_check, address review comments
2019-05-02Merge PR #10017: Exposing a change_no_check tacticPierre-Marie Pédrot
Ack-by: Zimmi48 Ack-by: herbelin Reviewed-by: ppedrot
2019-05-02Merge PR #10038: [comDefinition] Use prepare function from DeclareDef.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-05-02Merge PR #10047: [opam] [dune] Fix opam build by correctly setting prefix.Théo Zimmermann
Reviewed-by: Zimmi48
2019-05-02Remove outdated commentMaxime Dénès
2019-05-02Test case for #5752Maxime Dénès
2019-05-02Fix #5752: `Hint Mode` ignored for type classes that appear as assumptionsMaxime Dénès
The creation of the local hint db now inherits the union of the modes from the dbs passed to `typeclasses eauto`. We could probably go further and define in a more systematic way the metadata that should be inherited. A lot of this code could also be cleaned-up by defining the merge of databases, so that the search code is parametrized by just one db (the merge of the input ones).
2019-05-02Use GlobRef.Map.t in hint databasesMaxime Dénès
2019-05-02Add union in Map interfaceMaxime Dénès
2019-05-02Document typeclasses_eautoMaxime Dénès
2019-05-02Merge PR #10048: [CI/Azure/macOS] Fix install of OCaml through OPAMEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-05-02[CI/Azure/macOS] Fix install of OCaml through OPAMVincent Laporte
2019-05-02[opam] [dune] Fix opam build by correctly setting prefix.Emilio Jesus Gallego Arias
The OPAM build has been broken it seems since almost the beginning as OPAM doesn't substitute variables in the almost undocumented `build-env` form. Packages built this way worked as Coq used a different method to locate `coqlib`, however the value for `coqlib` was incorrect. We set instead the right prefix using an explicit configure call.
2019-05-01Add PairUsualDecidableTypeFullOliver Nash
A module allowing the user to build a UsualDecidableTypeFull from a pair of such, exactly analogous to the extant PairDecidableType and PairUsualDecidableType modules. Co-authored-by: Jean-Christophe Léchenet <eponier@via.ecp.fr>
2019-05-01[comDefinition] Use prepare function from DeclareDef.Emilio Jesus Gallego Arias
We also update the plugin tutorial. This was already tried [in the same exact way] in #8811, however the bench time was not convincing then, but now things seem a bit better, likely due to the removal of some extra normalization somewhere. Some more changes from #8811 are still pending.
2019-05-01Merge PR #10033: Remove the k0 argument from pretype functions.Emilio Jesus Gallego Arias
Reviewed-by: herbelin
2019-04-30Merge PR #9947: Remove Global.env from goptions by passing from vernacentriesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:25:50 +0000