aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-24Adapt to fix/cofix changes in Coq (coq/coq#7196)Emilio Jesus Gallego Arias
c.f. https://github.com/coq/coq/pull/7196
2018-05-24Merge PR #7574: Improve merging and overlay documentations.Emilio Jesus Gallego Arias
2018-05-24Remove the unused printer_pr mechanism.Jim Fehrle
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-24[ide] Move common protocol library to its own folder/object.Emilio Jesus Gallego Arias
The `ide` folder contains two different binaries, the language server `coqidetop` and `coqide` itself. Even if these binaries are in the same folder, the only thing they have in common is that they link to the protocol files. In the OCaml world, having "doubly" linked files in the same project is considered a bit of an ugly practice, and some build tools such as Dune disallow it.q Thus, to clean up the build, we move the common protocol files to its own library `ideprotocol`. This helps towards Dune integration and towards having an IDE standalone target, such as the one that was implemented here: https://github.com/ejgallego/coqide-exp
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-23Don't try to install native compiled files if native-compile is not setJim Fehrle
2018-05-24Merge PR #6515: [api] Move `Vernacexpr` to parsing.Pierre-Marie Pédrot
2018-05-23Fix #7586: Anomaly "Uncaught exception Not_found".Pierre-Marie Pédrot
The old unification engine was using the unfiltered environment when a context had been cleared, leading to an ill-typed goal.
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-23Fix #7576: broken link for Delahaye paper.Théo Zimmermann
2018-05-23Remove unused references from biblio.Théo Zimmermann
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-22Add myself as a secondary maintainer for the documentation.Théo Zimmermann
To reflect reality. [ci skip]
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 14:08:22 +0000