aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-19Merge PR #8999: [pfedit] Remove cook_proof stub.Pierre-Marie Pédrot
2018-11-19Merge PR #9023: [gramlib] Remove unused alias.Pierre-Marie Pédrot
2018-11-19Merge PR #9013: Do not Export the init modulesPierre-Marie Pédrot
2018-11-19Merge PR #8451: Print Universes SubgraphPierre-Marie Pédrot
2018-11-19Merge PR #7881: Reimplement Store using DynPierre-Marie Pédrot
2018-11-19[gramlib] Remove unused alias.Emilio Jesus Gallego Arias
No effect on actual code.
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[pfedit] Remove cook_proof stub.Emilio Jesus Gallego Arias
This is barely used and not very useful, clients should use the close_proof API directly.
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-16Use universe names when printing to dot.Gaëtan Gilbert
2018-11-16Print Universes SubgraphGaëtan Gilbert
This adds an optional [Subgraph] part to the Print Universes command, eg [Print Universes Subgraph(i j)] to print only constraints related to i and j (and Prop/Set).
2018-11-16Make UGraph printing independent of hash orderGaëtan Gilbert
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-16Do not Export the init modulesGaëtan Gilbert
It seems we started doing the export silently in 47804492bd09c8b13b5aac45800d067dbdf04d00.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:18:00 +0000