aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2018-11-09[dune] Build `cmxs` files instead of `cmxa` in "quick" target.Emilio Jesus Gallego Arias
This fixes #8954
2018-11-09[dune] [ide] Install data files.Emilio Jesus Gallego Arias
We should install the files in `share/coqide` instead of the current `coq` location; but we defer this change until we are more advanced in the make-phase out. Fixes: #8953
2018-11-09Fix -top for univbinders output test.Gaëtan Gilbert
It was good enough for the makefile but not for emacs.
2018-11-09Merge PR #8601: Move bound universe names to abstract contextsGaëtan Gilbert
2018-11-09Add .cmt and generated ml files to gitignoreGaëtan Gilbert
2018-11-09Adapt to coq/coq#8933 (Make initial evar map argument to ↵Gaëtan Gilbert
check_evars_are_solved optional)
2018-11-09Merge PR #8820: Standardize handling of Automatic Introduction.Pierre-Marie Pédrot
2018-11-09Merge PR #8408: [doc] [ssr] Fix renderingThéo Zimmermann
2018-11-09Fix dune runtest invocationGaëtan Gilbert
2018-11-09Add a test for bug #8939.Pierre-Marie Pédrot
2018-11-09Adding an overlay for #8601.Pierre-Marie Pédrot
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
There is little point in having a list, as there is virtually no sharing nor expansion of bound universe names. This representation is thus more compact.
2018-11-09Remove remnants of polymorphic instance name registration.Pierre-Marie Pédrot
2018-11-09Actually store the bound name information in the abstract universe context.Pierre-Marie Pédrot
2018-11-09Force the user to provide names when generating abstract universe contexts.Pierre-Marie Pédrot
For now this data is not stored, but the code checks that indeed the number of names provided coincide with the instance length. I had to reimplement the same kind of workaround hack in section handling as the one already performed in UnivNames because the name information is not present in the section data structure. This deserves a FIXME.
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-08Standardize handling of Automatic Introduction.Jasper Hugunin
This fixes #8791. We explicitly specify for intro the names of binders which are given by the user. This still can suffer from spurious collisions, see #8819.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 04:24:46 +0000