aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-19Fix dune checker file.Pierre-Marie Pédrot
2018-11-19Adding overlays.Pierre-Marie Pédrot
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Proper record type and accessors for transparent states.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-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
2018-11-19[proof] Provide better control of "open proofs" exceptions.Emilio Jesus Gallego Arias
2018-11-18[options] Remove deprecated option automatic introduction.Emilio Jesus Gallego Arias
2018-11-18merge-pr: Improve overlay checkGaëtan Gilbert
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 changing...Maxime Dénès
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
2018-11-17[vernacextend] Consolidate extension points APIEmilio Jesus Gallego Arias
2018-11-17[ci] Uniformize casing of makefile targets and ci variables.Emilio Jesus Gallego Arias
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
2018-11-17[CoqProject] Abstract warning function for CoqProject readers.Emilio Jesus Gallego Arias
2018-11-17[ltac] Use CAst nodes in the tactic AST.Emilio Jesus Gallego Arias
2018-11-16Remove SSR profilingJim Fehrle
2018-11-16Merge PR #8779: Remove the implicit tactic feature following #7229.Matthieu Sozeau
2018-11-16Print logs in appveyor test suite runGaëtan Gilbert
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
2018-11-16Make UGraph printing independent of hash orderGaëtan Gilbert
2018-11-16Print universe names in subtyping error instead of Var(x).Gaëtan Gilbert
2018-11-16We improve a little bit in printing universe constraints signature mismatch.Hugo Herbelin
2018-11-16Print full binders in subtyping incompatible polymorphism error.Gaëtan Gilbert
2018-11-16put protocol/ in ide/.merlinGaëtan Gilbert
2018-11-16No Projection.constant in projection <-> constant declarationGaëtan Gilbert
2018-11-16Heads: simplify using that projections are always rigidGaëtan Gilbert
2018-11-16Do not Export the init modulesGaëtan Gilbert
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
2018-11-15Make set_typing_flags "smart"Gaëtan Gilbert
2018-11-15Merge PR #8955: [ssr] "case/elim: p" don't resolve TC in "p"Vincent Laporte
2018-11-14Get hyps and goal the same way Printer does; don't omit infoJim Fehrle
2018-11-14Merge PR #8966: coq_makefile: Fix ocamldep ignoring mlg filesEmilio Jesus Gallego Arias