aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-10-25[default.nix] Update to dune 1.4.Théo Zimmermann
2018-10-25Merge PR #8762: [dune] [opam] Move to OPAM 2.0Gaëtan Gilbert
2018-10-24Merge PR #8813: Fix a few rendering issues in the manualThéo Zimmermann
2018-10-24Comment Environ.set_universesGaëtan Gilbert
I looked for this information and forgot about it a couple times so let's put it in writing.
2018-10-24Merge PR #8776: Replace non-idiomatic "dead-alleys" with idiomatic "dead-ends"Théo Zimmermann
2018-10-24[Manual] Prevent an irrelevant warning to show upVincent Laporte
2018-10-24[Manual] Avoid using deprecated “Focus”Vincent Laporte
2018-10-24[Manual] Fix rendering of an exampleVincent Laporte
2018-10-24[Manual] TypoVincent Laporte
2018-10-24[Manual] Fix an exampleVincent Laporte
The `Undo` command is not reliable.
2018-10-24[Manual] Fix layout of a listVincent Laporte
2018-10-24[Coqlib] Remove redundant checkVincent Laporte
2018-10-24[ssreflect] Better use of CoqlibVincent Laporte
- Look constants up using registered names - As lazily as possible
2018-10-23Merge PR #8806: Fixing #8794: anomaly with abbreviation binding both a term ↵Emilio Jesus Gallego Arias
and a binder
2018-10-23Merge PR #8365: Strings: add ByteVectorHugo Herbelin
2018-10-23[dune] [opam] Move to OPAM 2.0Emilio Jesus Gallego Arias
We need to update in Docker: - dune to 1.4.0: as it honors `-p` on test stanzas - dune-release to 1.1.0: support for OPAM 2.0 + fixes This makes `dune-release distrib` / `dune-release opam pkg` work. TODO: we need to figure out what is going on with the versioning. Should we do `dune subst` on `pinned`?
2018-10-23Merge PR #8798: Order Greek letters consistently w/rest of documentThéo Zimmermann
2018-10-23Merge PR #8799: Fix formatting. Use standard if..then grammar.Théo Zimmermann
2018-10-23Fixing #8794 (anomaly with abbreviation involving both term and binders).Hugo Herbelin
2018-10-23Merge PR #8802: [dune] Install man pages + remove two obsolete ones.Théo Zimmermann
2018-10-23Fix issue #8801.Guillaume Melquiond
When opening the query pane, do not try to focus on a query tab that no longer exists.
2018-10-23Fix issue #8800.Guillaume Melquiond
Gtk complains that we are not using gtk_scrolled_window_add_with_viewport, so let us do.
2018-10-23Merge PR #8786: Adding a regression test for bug #8785: universe constraints ↵Pierre-Marie Pédrot
missing
2018-10-23Compat 8.8: For String/Ascii, hides "Declare ML Module" behind an "Export".Hugo Herbelin
2018-10-23Encapsulating declarations of primitive string syntax in a module.Hugo Herbelin
2018-10-23Merge PR #8797: [doc] [api] Update `odoc` to new release 1.3.0Gaëtan Gilbert
2018-10-23Merge remote-tracking branch 'origin/pr/70'Pierre-Marie Pédrot
2018-10-23Merge remote-tracking branch 'origin/pr/71'Pierre-Marie Pédrot
2018-10-23[dune] Install man pages + remove two obsolete ones.Emilio Jesus Gallego Arias
2018-10-23Fix formatting. Use standard if..then grammar.Sam Pablo Kuper
2018-10-23Order Greek letters consistently w/rest of documentSam Pablo Kuper
2018-10-23[dune] Compile debug and checker printers.Emilio Jesus Gallego Arias
As noted by Gäetan, we didn't compile these. We also provide a recipe to run `ocamldebug`. Try (after a build): ``` dune exec dev/dune-dbg (ocd) source dune_db ``` or ``` dune exec dev/dune-dbg checker (ocd) source checker_dune_db ``` for the checker.
2018-10-23[build] Refactoring to config lib and ocamldebug tweaks.Emilio Jesus Gallego Arias
We make `config` into a properly library. This is more uniform and useful for some clients. This also matches what was done in Dune. Next step would be to push dependencies on `Coq_config` upwards, only the actual toplevel binaries should depend on it. We also remove the stale `camlp5.dbg` and refactor the dbg files a bit, isolating the bits that are specific to the plugin / lib building method used by makefile.
2018-10-22[doc] [api] Update `odoc` to new release 1.3.0Emilio Jesus Gallego Arias
This includes many changes, please have a look at the newly generated docs.
2018-10-22Merge PR #8708: Stupid but critical unfolding heuristic.Maxime Dénès
2018-10-22Merge PR #8784: [dune] Remove rule for cLexer.ml4 -> cLexer.mlThéo Zimmermann
2018-10-22Merge pull request #11 from ejgallego/vernac+monify_hookYves Bertot
[coq] Adapt for PR #8704.
2018-10-21Adding a regression test for bug #8785 (missing univ constraints registration).Hugo Herbelin
2018-10-20Cleanup comparing projections through their constants.Gaëtan Gilbert
2018-10-20Merge PR #8769: [library] Remove redundant re-addition of universe constraints.Gaëtan Gilbert
2018-10-20[dune] Remove rule for cLexer.ml4 -> cLexer.mlEmilio Jesus Gallego Arias
When merging #8740 we didn't remove this rule. The build didn't fails as Dune emits a warning for now [due to compatibility with some schemes], but this will become an error in the future.
2018-10-20Merge PR #8782: gitignore test-suite/.nia.cacheThéo Zimmermann
2018-10-19Merge PR #8758: [api] Qualify access to `Nametab`Hugo Herbelin
2018-10-19gitignore test-suite/.nia.cacheGaëtan Gilbert
This gets generated since 7f445d1027cbcedf91f446bc86afea36840728ba
2018-10-19Deprecating unused Engine.type_of_global.Hugo Herbelin
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
Removing a few Global.env in the way.
2018-10-19Deprecating Global.constr_of_global_in_context.Hugo Herbelin
2018-10-19Moving Global.constr_of_global_in_context to Typeops.Hugo Herbelin
It is purely functional, so no need for it to be in global now that GlobRef.t are in the kernel.
2018-10-19Moving Global.type_of_global_in_context to Typeops.Hugo Herbelin
It is purely functional, so no need for it to be in global now that GlobRef.t are in the kernel. Also updated the comments.
2018-10-19Cleaning layout typeops.mli.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-20 01:21:44 +0000