aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-03-08Merge PR #6934: Warn when using “Require” in a sectionMaxime Dénès
2018-03-08Merge PR #6924: Clean-up remove always false useeager argument.Maxime Dénès
2018-03-08Merge PR #6902: [compat] Remove "Discriminate Introduction"Maxime Dénès
2018-03-08Merge PR #6903: [compat] Remove "Shrink Abstract"Maxime Dénès
2018-03-08Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Maxime Dénès
2018-03-07Use a proper warning when a summary is captured out of module scope.Vincent Laporte
2018-03-07[vernac] Warn when using “Require” in a sectionVincent Laporte
2018-03-07[stdlib] Do not use “Require” inside sectionsVincent Laporte
2018-03-07Merge PR #6744: Add String.concatMaxime Dénès
2018-03-07Merge PR #6932: [stdlib] Do not use deprecated notationsMaxime Dénès
2018-03-07Merge PR #6905: Fix make ml-docMaxime Dénès
2018-03-07Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Maxime Dénès
2018-03-07Merge PR #6922: Remove outdated information regarding the FAQ.Maxime Dénès
2018-03-07Merge PR #6374: [toplevel] Modify printing goal strategy.Maxime Dénès
2018-03-07Merge PR #6790: Allow universe declarations for [with Definition].Maxime Dénès
2018-03-07Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Maxime Dénès
2018-03-06[stdlib] Do not use deprecated notationsVincent Laporte
2018-03-06Clean-up remove always false useeager argument.Théo Zimmermann
2018-03-06Remove outdated information regarding the FAQ.Théo Zimmermann
The FAQ is not part of the Coq sources anymore.
2018-03-06Merge PR #6917: Fix failing packaging job.Maxime Dénès
2018-03-06[compat] Remove "Discriminate Introduction"Emilio Jesus Gallego Arias
Following up on #6791, we the option "Discriminate Introduction".
2018-03-06[compat] Remove "Shrink Abstract"Emilio Jesus Gallego Arias
Following up on #6791, we the option "Shrink Abstract".
2018-03-06Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ↵Maxime Dénès
a record.
2018-03-06Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.Maxime Dénès
2018-03-06ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Enrico Tassi
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-06Merge PR #6900: [compat] Remove "Tactic Pattern Unification"Maxime Dénès
2018-03-06Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Maxime Dénès
2018-03-06Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"Maxime Dénès
2018-03-05[toplevel] Modify printing goal strategy.Emilio Jesus Gallego Arias
Instead of using a command-analysis heuristic, coqtop will now print goals if the goal has changed. We use a fast goal comparison heuristic, but a more refined strategy would be possible. This brings some [IMHO very welcome] change to PG and `-emacs`, which will now disable the printing of goals. Now, instead of playing with `Set/Unset Silent` and a bunch of other hacks, PG can issue a `Show` command whenever it wishes to redisplay the goals. This change will break PG, so we need to carefully coordinate this PR with PG upstream (see ProofGeneral/PG#212). Some interesting further things to do: - Detect changes in nested proofs. - Uncouple the silent flag from "print goals".
2018-03-05Fix failing packaging job.Théo Zimmermann
gtksourceview depends transitively on py2cairo which was updated in Homebrew to depend explicitly on python2 (see Homebrew/homebrew-core#24714): this makes the python3 install step impossible. We also remove the libxml2 install step which was failing in a non-fatal way.
2018-03-05Remove NOPLUGINDOCS optionmrmr1993
2018-03-05Add empty description for @raise statements to satisfy ocamldocmrmr1993
2018-03-05Escape curly braces in ocamldoc commentmrmr1993
2018-03-05Separate vim/emacs fold markers from ocamldoc commentsmrmr1993
ocamldoc chokes on the markers {{{ and }}} because { and } are part of its syntax
2018-03-05Build docs for plugins by default, add NOPLUGINDOCS flag to disablemrmr1993
2018-03-05Change non-documentation comment from ocamldoc stylemrmr1993
2018-03-05Fix formatting of some ocamldoc comments to reduce warningsmrmr1993
2018-03-05Replace invalid tag @raises in ocamldoc comments with @raisemrmr1993
2018-03-05Remove non-existent dependencymrmr1993
2018-03-05Tweak comments to fix ocamldoc errorsmrmr1993
2018-03-05Tidy up ml-doc outut, give it a separate output directorymrmr1993
2018-03-05Use computed deps to generate ml-doc and use implicit mli-doc depsmrmr1993
2018-03-05CHANGES and tests for with Definition @{univs}Gaëtan Gilbert
2018-03-05Allow universe declarations for [with Definition].Gaëtan Gilbert
2018-03-05[ssreflect] Export parsing witnesses in mli file.Emilio Jesus Gallego Arias
This is needed in order to manipulate/serialize SSR's AST. A quicker [and maybe better] alternative would be to just remove `ssrparser.mli`, as there are many grammar entries that still need exporting.
2018-03-05Sanitize universe declaration in Context (stop using a ref...)Gaëtan Gilbert
When there is more than one variable to declare we stop trying to attach global universes (ie monomorphic or section polymorphic) to one of them.
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-05Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 00:03:34 +0000