aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-07-07Merge PR #12626: Fix Context with nonmaximplicit.Emilio Jesus Gallego Arias
2020-07-06Merge PR #11604: Primitive persistent arraysPierre-Marie Pédrot
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-06Merge PR #12622: Use goal cycling instead of manual evar generation order in ...Gaëtan Gilbert
2020-07-05Merge PR #12641: Windows build: use architecture dependent version of windresEnrico Tassi
2020-07-05Merge PR #12594: Fix ltac2 type parametersMichael Soegtrop
2020-07-05Merge PR #12613: Remove deprecated (in 8.8 #6277) coqchk -IPierre-Marie Pédrot
2020-07-04Windows build: remove patch for windres architectureMichael Soegtrop
2020-07-04Windows build: use architecture dependent version of windresMichael Soegtrop
2020-07-03Merge PR #12523: Fix #11121: Simultaneous definition of term and notation in ...Gaëtan Gilbert
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
2020-07-02Merge PR #12628: Fix debug printer for auctx in presence of AnonymousEmilio Jesus Gallego Arias
2020-07-02Merge PR #12614: Cleanup mentions of -as in coqdep usage messageEmilio Jesus Gallego Arias
2020-07-02Fix debug printer for auctx in presence of AnonymousGaëtan Gilbert
2020-07-02Fix Context with nonmaximplicit.Gaëtan Gilbert
2020-07-02Merge PR #12572: Correctly classify variables as being unfoldable in dnet pat...Gaëtan Gilbert
2020-07-02Merge PR #12620: [state] Consolidate state handling into VernacstateGaëtan Gilbert
2020-07-02Merge PR #12618: Use weak ref to memoize Evarutil.is_ground_envPierre-Marie Pédrot
2020-07-01Use goal cycling instead of manual evar generation order in internal_cut_rev.Pierre-Marie Pédrot
2020-07-01[state] Consolidate state handling in VernacstateEmilio Jesus Gallego Arias
2020-07-01Add a changelog.Pierre-Marie Pédrot
2020-07-01Add a test for Ltac2 parsing of parameterized types.Pierre-Marie Pédrot
2020-07-01Factorize tac2type syntax to fix the parsing of (t1, ..., tn) t.Pierre-Marie Pédrot
2020-07-01Overlays for UIP in SPropGaëtan Gilbert
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Merge PR #12504: [states] Move States to vernacGaëtan Gilbert
2020-07-01Remove deprecated (in 8.8 #6277) coqchk -IGaëtan Gilbert
2020-07-01Merge PR #12605: [test-suite] async-proofs off in tests with Fail TimeoutGaëtan Gilbert
2020-07-01Merge PR #12615: [ci] [performance-tests] Use a lighter target.Gaëtan Gilbert
2020-07-01Use weak ref to memoize Evarutil.is_ground_envGaëtan Gilbert
2020-07-01Merge PR #12616: [ci] Disable the OCaml 4.12 targetGaëtan Gilbert
2020-07-01Merge PR #12596: Credit Erik Martin-Dorel for work on Docker.Emilio Jesus Gallego Arias
2020-07-01[ci] Disable the OCaml 4.12 targetEmilio Jesus Gallego Arias
2020-06-30Cleanup mentions of -as in coqdep usage messageGaëtan Gilbert
2020-06-30[ci] [performance-tests] Use a lighter target.Emilio Jesus Gallego Arias
2020-06-30Merge PR #12599: Remove the Refiner moduleEmilio Jesus Gallego Arias
2020-06-30[declaremods] Remove abstraction of imperative module operationsEmilio Jesus Gallego Arias
2020-06-30[states] Move States to vernacEmilio Jesus Gallego Arias
2020-06-30Merge PR #11977: Generate default names for bound universes of polymorphic de...Emilio Jesus Gallego Arias
2020-06-29[test-suite] async-proofs off in tests with Fail TimeoutEnrico Tassi
2020-06-29Merge PR #12570: CoqIDE: fix lexing of UTF-8 in quotations like constr:()Pierre-Marie Pédrot
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
2020-06-29Adding overlay.Pierre-Marie Pédrot
2020-06-29Refining out the Refiner.Pierre-Marie Pédrot
2020-06-29Move the FailError exception from Refiner to Tacticals.Pierre-Marie Pédrot
2020-06-29Moving the remaining Refiner functions to Tacmach.Pierre-Marie Pédrot
2020-06-29Remove Refiner.refiner.Pierre-Marie Pédrot
2020-06-29Remove the deprecated functions from refiner, moving them to Tacticals.Pierre-Marie Pédrot
2020-06-29Merge PR #12604: Update CAMLDONTLINK in CoqMakefile.inEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 23:44:22 +0000