aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-16Add test for Include in -quick modeGaëtan Gilbert
2018-11-16Don't redeclare constraints of fields in IncludeGaëtan Gilbert
2018-11-16Termops.iter_constr_with_full_binders = EConstr.iter_with_full_bindersGaëtan Gilbert
2018-11-16Share open recursor code between econstr and constrGaëtan Gilbert
2018-11-16Fix lifting in foo_with_full_binders for (co)fixpointsGaëtan Gilbert
2018-11-16Small simplification in fold_constr_with_bindersGaëtan Gilbert
2018-11-16Remove some univ_flexible_alg from casesGaë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-15Fix compilation w.r.t. coq/coq#8779.Pierre-Marie Pédrot
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
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
2018-11-14Update .mailmap.Théo Zimmermann
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
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
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 extensi...Pierre-Marie Pédrot
2018-11-13[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 08:15:39 +0000