aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-14ssr: add another test for elim + TCEnrico Tassi
2018-11-14ssr: rewrite: do resolve TC once and forall at the very endEnrico Tassi
2018-11-14ssr: elim: do resolve TC once and forall at the very endEnrico Tassi
2018-11-14ssrcommon: API to call resolve_tyclasses on a termEnrico Tassi
2018-11-14ssrmatching: unify_HO does not resolve type classesEnrico Tassi
2018-11-14[mailmap] Update "anonymous" accounts.Théo Zimmermann
Of the three "anonymous" accounts, one ("coq") was used by multiple authors (in particular Jacek Chrząszcz who developed the module system), while the other two are each the committer of a single auto-generated commit so we rename them to cvs2svn and serpyc-bot.
2018-11-14Update .mailmap.Théo Zimmermann
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
Previously, hints added without a specified database where implicitly put in the "core" database, which was discouraged by the user manual (because of the lack of modularity of this approach).
2018-11-13Merge PR #8886: [VM] Fix compilation of int31 eliminatorsMaxime Dénès
2018-11-13Merge PR #8906: [Goptions] More detailed error messagesMaxime Dénès
2018-11-13Merge PR #8760: Automatically generate names for universes.Pierre-Marie Pédrot
2018-11-13coq_makefile: Fix ocamldep ignoring mlg filesGaëtan Gilbert
If you have file1.mlg and file2.ml, with file2 depending on file1, ocamldep was before generating file1.ml so wouldn't generate [file2.cmx: file1.cmx] (ocamldep is silent on non-found dependencies). This has been causing nondeterministic failures in quickchick recently. I guess it didn't come up in the past because ml4 files tend to be at the end of the dependency chain.
2018-11-13Merge PR #8976: CoqHammer CIGaëtan Gilbert
2018-11-13Merge PR #8957: Fix -top for univbinders output test.Emilio Jesus Gallego Arias
2018-11-13Port to coqpp.Pierre-Marie Pédrot
2018-11-13Merge PR #8919: [vernac] Rename Vernacinterp to Vernacextend and move ↵Pierre-Marie Pédrot
extension functions there
2018-11-13[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.Emilio Jesus Gallego Arias
This PR fixes an issues that was bugging me for some time, namely that `Vernacinterp` really means `Vernacextend`. We thus rename the file and move the associated functions there, which were incorrectly placed in `Vernacentries`. Note the beneficial effects on reducing the `.mli` API.
2018-11-13[configure] Remove grammar and dev from core_src_dirs.Emilio Jesus Gallego Arias
These directories don't contain Coq sources but internal developer files. This can create problems, for example, in #8919.
2018-11-13Merge PR #8978: nix helpers for debugging external projects from CIEmilio Jesus Gallego Arias
2018-11-13Merge PR #8936: Fix #8908: incorrect refresh of algebraic universes.Pierre-Marie Pédrot
2018-11-12Merge PR #8979: Skip submodules in HoTT CI script.Emilio Jesus Gallego Arias
2018-11-12Merge PR #8960: [dune] Build `cmxs` files instead of `cmxa` in "quick" target.Enrico Tassi
2018-11-12Skip submodules in HoTT CI script.Gaëtan Gilbert
Avoid downloading Coq.
2018-11-12Automatically generate names for universes.Gaëtan Gilbert
The names are `uXXX` with `XXX` some number avoiding collision. Note that there may be some collisions with polymorphic binders, eg something like ~~~ Set Universe Polymorphism. Section foo. Universe u0. Definition bar := Type. (* bar@{u0} = Type@{u0} but this isn't the section u0 *) Definition baz := Type@{u0}. (* this one is the section u0 *) Definition foobar := Eval compute in baz -> Type. (* Type@{u0} -> Type@{u0} but these aren't the same u0 *) ~~~ So maybe we should do a nametab lookup too. This is strictly a printing issue (polymorphic binder names have no other use). In the monomorphic case names are qualified by the parent definition so it should be fine (barring module/definition collision but we already have those). Note that there are still unnamed universes as they didn't go through UState (eg schemes).
2018-11-12Do not qualify universe names by section path.Gaëtan Gilbert
2018-11-12Fix incorrect coq-prog-args in unideclsGaëtan Gilbert
2018-11-12Don't declare universe binders for variables.Gaëtan Gilbert
Otherwise ~~~ Unset Strict Universe Declaration. Section bar. Let baz := Type@{u}. Definition k := baz. End bar. Section bar. Let baz := Type@{u}. Definition k' := baz. End bar. ~~~ is broken (and has been since we stopped checking for repeated section names).
2018-11-12Only declare univ binders once for mutindGaëtan Gilbert
2018-11-12Merge PR #8962: [ci] Add paramcoq to CI.Gaëtan Gilbert
2018-11-12Merge PR #8892: Fix part of #8224: grounding open term in fixpointsPierre-Marie Pédrot
2018-11-12Merge PR #8972: Fix #4771: Substitution of inline global reference in ↵Pierre-Marie Pédrot
tactics is broken
2018-11-12CoqHammer CILukasz Czajka
2018-11-12Set codeowners for dev/ci/nixVincent Laporte
2018-11-12Helpers for debugging external projects from CIVincent Laporte
2018-11-12Merge PR #8938: [Plugins] Remove some dead codePierre-Marie Pédrot
2018-11-12Merge PR #8958: [clib] Remove unneeded `get_extension` function.Pierre-Marie Pédrot
2018-11-12Test case for #4771: Substitution of inline global reference in tactics is ↵Maxime Dénès
broken
2018-11-12Fix #4771: Substitution of inline global reference in tactics is brokenMaxime Dénès
2018-11-12Fix #8908: incorrect refresh of algebraic universes.Gaëtan Gilbert
2018-11-12[clib] Remove unneeded `get_extension` function.Emilio Jesus Gallego Arias
This has been in OCaml since 4.04.
2018-11-11CoqIDE: pass the parent window to all methods liable to open a question box.Hugo Herbelin
This is to ensure that the corresponding question boxes remains in front of the main window, consistently with the fact that they are blocking actions on the main window.
2018-11-11A private copy of lablgtk's question_box supporting the "parent" option.Hugo Herbelin
The "parent" option allows to attach the box to the parent box. This ensures that the dialog box, which blocks action on the main window, does not get hidden by the main window. Idem for the message_box.
2018-11-11CoqIDE: ensure that the configuration box is not hidden by the main window.Hugo Herbelin
We do it by passing the name of the main window in the "parent" option. Formerly, the window could be hidden but nevertheless blocking any action on the main window. With the change, it can be moved aside, but never hidden by the main window. Tested on MacOS X.
2018-11-11CoqIDE: remove obselete menu item "Complete word".Hugo Herbelin
This was obsolete since new completion in 945d7db9 (then a07359f6).
2018-11-11CoqIDE: Do not rebind up and down in microPG mode.Hugo Herbelin
First, they already work by default. Second, by rebinding them, they cannot be used any longer in the completion menu, which is a bit annoying.
2018-11-11Merge PR #8795: Encapsulating declarations of primitive string syntax in a ↵Jason Gross
module
2018-11-10[ci] Add paramcoq to CI.Emilio Jesus Gallego Arias
2018-11-09Merge PR #8949: Remove checker printersEmilio Jesus Gallego Arias
2018-11-09Merge pull request #19 from SkySkimmer/gitignoreEmilio Jesús Gallego Arias
Add .cmt and generated ml files to gitignore
2018-11-09Merge PR #8956: Fix dune runtest invocationEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-26 18:45:23 +0000