aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-25Fix notation for code snippet in documentationAnton Trunov
It failed to compile before because the type arguments were declared implicit after introducing the notation
2018-05-25Merge PR #7556: Add a setting to warn about empty object in the refmanMaxime Dénès
2018-05-25Merge PR #7508: Improve rewrite section in tactic chapter.Maxime Dénès
2018-05-25Merge PR #7533: [sphinx] Bump timeout. Closes #7532.Maxime Dénès
2018-05-25Merge PR #7196: [tactics] Remove anonymous fix/cofix form.Pierre-Marie Pédrot
2018-05-25Merge PR #7325: Fix #7323: coqchk puts polymorphic univs of inductive in ↵Pierre-Marie Pédrot
global env
2018-05-25Merge PR #7598: Fix recipe for FAKEIDEBYTEEnrico Tassi
2018-05-24[tactics] Remove anonymous fix/cofix form.Emilio Jesus Gallego Arias
We remove the `fix N / cofix N` forms from the tactic language. This way, these tactics don't depend anymore on the proof context, in particular on the proof name, which seems like a fragile practice. Apart from the concerns wrt maintenability of proof scripts, this also helps making the "proof state" functional; as we don't have to propagate the proof name to the tactic layer.
2018-05-24Fix recipe for FAKEIDEBYTEGaëtan Gilbert
Caused by a semantic conflict with the separate toplevels PR.
2018-05-24Merge PR #7574: Improve merging and overlay documentations.Emilio Jesus Gallego Arias
2018-05-24Complete rewrite of the documentation of overlays after Jim's additional ↵Théo Zimmermann
comments. [ci skip]
2018-05-24Relax advice on the name of user-overlays following Gaëtan's suggestion.Théo Zimmermann
[ci skip]
2018-05-24Improve merging and overlay documentations.Théo Zimmermann
Clarification prompted by Jim Fehrle. [ci skip]
2018-05-24Merge PR #7177: Unifying names of "smart" combinators + adding combinators ↵Pierre-Marie Pédrot
in CArray
2018-05-24Merge PR #7594: Fix #5983 (many frequent AppVeyor failures) by increasing ↵Emilio Jesus Gallego Arias
spawn timeout.
2018-05-24Fix #7323: coqchk puts polymorphic univs of inductive in global envGaëtan Gilbert
2018-05-24Merge PR #7581: Mention warning and error message docs in PR templateThéo Zimmermann
2018-05-24Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constantsPierre-Marie Pédrot
2018-05-24Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant ↵Pierre-Marie Pédrot
instances
2018-05-24Merge PR #7575: [build] Add -cclib -lcoqrun options to build of kernel.cmxa.Enrico Tassi
2018-05-24Fix #5983 (many frequent AppVeyor failures) by increasing spawn timeout.Théo Zimmermann
2018-05-24Merge PR #7582: [ci] Build fiat-crypto targets in sequenceEmilio Jesus Gallego Arias
2018-05-24Merge PR #6515: [api] Move `Vernacexpr` to parsing.Pierre-Marie Pédrot
2018-05-23Document Smart/Array changes in dev/doc/Changes.md.Hugo Herbelin
2018-05-23Renaming miscellaneous internal smart functions.Hugo Herbelin
2018-05-23Collecting Map.smart_* functions into a module Map.Smart.Hugo Herbelin
2018-05-23Moving Rtree.smart_map into Rtree.Smart.map.Hugo Herbelin
2018-05-23Moving Option.smart_map to Option.Smart.map.Hugo Herbelin
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-23Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Hugo Herbelin
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-23Emphasizing the "smart"ness of Array.smartfoldmap{,2} in their documentation.Hugo Herbelin
This follows the model of smartmap and smartmap2.
2018-05-23CArray: adding combinators.Hugo Herbelin
2018-05-23Remove dashes from PR templateJason Gross
As per PR comment suggestion
2018-05-23[api] Move `Vernacexpr` to parsing.Emilio Jesus Gallego Arias
There were a few spurious dependencies on the `Vernac` AST in the pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing, where they do belong more.
2018-05-23[api] Move `opacity_flag` to `Proof_global`.Emilio Jesus Gallego Arias
`Proof_global` is the main consumer of the flag, which doesn't seem to belong to the AST as plugins show. This will allow the vernac AST to be placed in `vernac` indeed.
2018-05-23Merge PR #7414: Add .byte targets for every bestocaml targetEnrico Tassi
2018-05-23Merge PR #7567: Clean-up dead file in test-suite.Enrico Tassi
2018-05-22[ci] Build fiat-crypto targets in sequenceJason Gross
This should hopefully alleviate memory problems on gitlab, by first building the `lite` targets, and then building the remaining not-that-big targets.
2018-05-22Merge PR #7565: Document the new nested-proof error message.Emilio Jesus Gallego Arias
2018-05-22Merge PR #7577: Fixing debugger after #6859 (loading dynlink.cma before ↵Emilio Jesus Gallego Arias
lib.cma).
2018-05-22Mention warning and error message docs in PR templateJason Gross
This closes #7580 c.f. https://github.com/coq/coq/pull/7559#issuecomment-390749207 and https://github.com/coq/coq/pull/7559#issuecomment-390872924. This should be reverted if and when we move to autogenerated docs for warnings and errors, as suggested in #7373.
2018-05-22Fixing debugger after #6859 (loading dynlink.cma before lib.cma).Hugo Herbelin
2018-05-22[doc] Document the new report_undocumented_coq_objects settingClément Pit-Claudel
2018-05-22[doc] Add a list of common mistakesClément Pit-Claudel
2018-05-22[doc] Fix an incorrect use of $PWD in Makefile.docClément Pit-Claudel
2018-05-22[doc] Add a setting to warn about empty Coq objectsClément Pit-Claudel
2018-05-22Merge PR #7384: Split UniversesPierre-Marie Pédrot
2018-05-22Merge PR #7324: Infrastructure for ocamldebug on the checkerHugo Herbelin
2018-05-22Merge PR #7526: [circle] Use Docker image from Gitlab registry.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:52:56 +0000