aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-19Merge PR #7881: Reimplement Store using DynPierre-Marie Pédrot
2018-11-18Merge PR #9018: [devtools] Small script to setup overlays automaticallyGaëtan Gilbert
2018-11-17Merge PR #8712: [stm] avoid unshare safe env to detect correctly env ↵Maxime Dénès
changing tactics
2018-11-17Merge PR #8992: put protocol/ in ide/.merlinPierre-Marie Pédrot
2018-11-17Merge PR #8914: [CoqProject] Abstract warning function for CoqProject readers.Pierre-Marie Pédrot
2018-11-17[devtools] Small script to setup overlays automaticallyEmilio Jesus Gallego Arias
This is very preliminary but you should get the idea. The script tries to build contribs, then creates a branch and sets the remote properly as to submit a PR. Usage example: ``` ./dev/tools/create_overlays.sh ejgallego 9999 ltac2 elpi ``` This only works for contributions hosted in github for now.
2018-11-17[ci] Uniformize casing of makefile targets and ci variables.Emilio Jesus Gallego Arias
This is convenient as to have better automation.
2018-11-17[ci] Cleanup of old overlays.Emilio Jesus Gallego Arias
2018-11-17Merge PR #8968: Miscellaneous CoqIDE fixesPierre-Marie Pédrot
2018-11-17[CoqProject] Abstract warning function for CoqProject readers.Emilio Jesus Gallego Arias
`CoqProject_file` uses the feedback system, however this is not very convenient in some scenarios such as `coqdep` that has to be run very early in the build process [and thus in "boot" mode]. We thus make the warning function a paramater. Should fix #8913.
2018-11-16Merge PR #8779: Remove the implicit tactic feature following #7229.Matthieu Sozeau
2018-11-16Merge PR #8781: Remove primproj <-> constant dependency in HeadsPierre-Marie Pédrot
2018-11-16Reimplement Store using Dyn.whitequark
2018-11-16Add Dyn.anonymous, a more efficient version of Dyn.create (string_of_int n).whitequark
2018-11-16put protocol/ in ide/.merlinGaëtan Gilbert
2018-11-16No Projection.constant in projection <-> constant declarationGaëtan Gilbert
Enabled by previous commit about Heads.
2018-11-16Heads: simplify using that projections are always rigidGaëtan Gilbert
This avoids using Projection.constant in kind_of_head, which then allows compute_head to not check whether the constant is a compatibility definition (as in that case its body is [fun ... => x.(p)]). Thus Heads stops caring about the compatibility projection system.
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-11-16Merge PR #8888: Proof runcountable rebaseHugo Herbelin
2018-11-15Merge PR #8991: coqide: use correct toplevel name in filesEmilio Jesus Gallego Arias
2018-11-15Move generating library dirpath to stm in compile mode.Gaëtan Gilbert
2018-11-15coqide: use correct toplevel name in filesGaëtan Gilbert
Fix #8989. This adds an option -topfile taking a path so that inferring the right dirpath is done by the toplevel after processing -Q/-R instead of the client having to do it.
2018-11-15Make set_typing_flags "smart"Gaëtan Gilbert
Fix #8609 gares said: I believe it was introduced in de20a45 where the option (part of the summary) is moved to the save env. By setting the summary, you unshare the safe env. Now we do that only if needed. The stm uses `==` on the safe env to detect tactics that alter the env, eg abstract.
2018-11-15Merge PR #8955: [ssr] "case/elim: p" don't resolve TC in "p"Vincent Laporte
2018-11-14Merge PR #8966: coq_makefile: Fix ocamldep ignoring mlg filesEmilio Jesus Gallego Arias
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 07:46:46 +0000