aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-06-23Merge PR #12562: CoqIDE: accept to open files with invalid namesMichael Soegtrop
2020-06-23Merge PR #12530: Fix glob_sort_family for SPropMaxime Dénès
2020-06-23Fix #4459 by improving `par:` error messageMaxime Dénès
2020-06-23Merge PR #12552: Add a pre-hook mechanism for the `zify` tacticFrédéric Besson
2020-06-23Merge PR #8796: Elementary properties about IZR for generic useGaëtan Gilbert
2020-06-23CoqIDE: fix lexing of UTF-8 in quotations like constr:()James Lottes
2020-06-23Add a test for the strange behaviour encountered with this change.Pierre-Marie Pédrot
2020-06-23Use the unification result for eauto's eapply.Pierre-Marie Pédrot
2020-06-22Merge PR #12520: Cleanup the autorewrite implementationHugo Herbelin
2020-06-22Elementary properties about IZR for generic use.Hugo Herbelin
2020-06-22Merge PR #12434: Slight improvement in naming dependent existential variables...Gaëtan Gilbert
2020-06-22Merge PR #12555: Add test-suite/redirect_test.out file to .gitignoreGaëtan Gilbert
2020-06-22Merge PR #12546: [ci] Use a tested branch of PerennialEmilio Jesus Gallego Arias
2020-06-22CoqIDE: accept to open files with invalid namesVincent Laporte
2020-06-21Merge PR #12505: Cleanup the Hints APIHugo Herbelin
2020-06-21Merge PR #12559: Add index for coqdoc.Clément Pit-Claudel
2020-06-21Add index for coqdoc.Théo Zimmermann
2020-06-21Add a generated file to .gitignoreJason Gross
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-20Merge PR #12407: Fix #12406: fix Coq type error in dependent induction's LtacAnton Trunov
2020-06-19Merge PR #12531: Fast inductive compilationGaëtan Gilbert
2020-06-19Merge PR #12502: Preserve sharing in evar instancesGaëtan Gilbert
2020-06-19Add overlays.Pierre-Marie Pédrot
2020-06-19Move the hint polymorphic status to the hint instance.Pierre-Marie Pédrot
2020-06-19Wrap the content of full hints into a record.Pierre-Marie Pédrot
2020-06-19Remove access to hint section variables.Pierre-Marie Pédrot
2020-06-19Opacify the type of hint metadata.Pierre-Marie Pédrot
2020-06-19Remove dead code in the Hints API.Pierre-Marie Pédrot
2020-06-19Do not export Hints.make_extern.Pierre-Marie Pédrot
2020-06-19Do not export flags in Hints.make_resolves.Pierre-Marie Pédrot
2020-06-19Do not be verbose when declaring subclass hints.Pierre-Marie Pédrot
2020-06-19Factorize hint flags in Class_tatcis.make_make_resolve_hyp.Pierre-Marie Pédrot
2020-06-19Try to preserve more sharing in nf_evars_and_universes_opt_subst.Pierre-Marie Pédrot
2020-06-19Share the identity instance in pretyping environments.Pierre-Marie Pédrot
2020-06-19Do not reallocate named_context_val of the pretyping environment.Pierre-Marie Pédrot
2020-06-18Fix #12228 negative integers not accepted in ltac integer_listPierre Roux
2020-06-18Merge PR #12536: tactics.rst: fix typo — readd `cbv` to title of its sectionThéo Zimmermann
2020-06-17[ci] Use a tested branch of PerennialTej Chajed
2020-06-17tactics.rst: readd `cbv`Paolo G. Giarrusso
2020-06-17Merge PR #12508: Fix #12507 Anomaly when using a ssreflect `reflect` viewCyril Cohen
2020-06-17Merge PR #12506: [toplevel] Annotate tailcall functionsEnrico Tassi
2020-06-17Use an efficient data structure for VM compilation indexing.Pierre-Marie Pédrot
2020-06-17Check duplicity of constructor names in an algorithmically efficient way.Pierre-Marie Pédrot
2020-06-17Fix glob_sort_family for SPropGaëtan Gilbert
2020-06-16Use evar clauses instead of meta clauses in Autorewrite hint registration.Pierre-Marie Pédrot
2020-06-16Code simplification in Autorewrite.Pierre-Marie Pédrot
2020-06-16Remove dead code in autorewrite.Pierre-Marie Pédrot
2020-06-16make the linter happyEnrico Tassi
2020-06-15Merge PR #12509: updated ci for unicoqThéo Zimmermann
2020-06-15updated ci for unicoqbeta
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 20:04:21 +0000