aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-07-10Merge PR #12666: Add test for #10890 derive vs abstractEmilio Jesus Gallego Arias
2020-07-10Merge PR #12537: Take into account the existing delta-resolver when starting ...Gaëtan Gilbert
2020-07-09Merge PR #12542: Defined arbitrary base logarithms (Rlog) and added natural l...Michael Soegtrop
2020-07-09Add test for #10890 derive vs abstractGaëtan Gilbert
2020-07-09Merge PR #11836: [obligations] Functionalize Program stateGaëtan Gilbert
2020-07-08Merge PR #12627: Fix Canonical with universe polymorphism and primitive proje...Enrico Tassi
2020-07-08declare: Add [save_regular] API for obligation-ignoring proofsGaëtan Gilbert
2020-07-08[ci] Overlay for metacoq and rewriterEmilio Jesus Gallego Arias
2020-07-08[declare] Allow obligations update on equations closing hook.Emilio Jesus Gallego Arias
2020-07-08[obligations] Allow to simultaneously open a proof and add obligationsEmilio Jesus Gallego Arias
2020-07-08[obligations] Allow state-modifying hooksEmilio Jesus Gallego Arias
2020-07-08[obligations] Remove duplicate progmap_remove.Emilio Jesus Gallego Arias
2020-07-08[obligations] Functionalize Program stateEmilio Jesus Gallego Arias
2020-07-08[declare] Generalize type of hooks.Emilio Jesus Gallego Arias
2020-07-08Adding change log.Hugo Herbelin
2020-07-08Adding test for #12525 (Search of lemmas in Include failing when in Module).Hugo Herbelin
2020-07-08Merge PR #12612: docs(README.md): Update badge and linksEmilio Jesus Gallego Arias
2020-07-08Merge PR #12654: Reindent ppvernac.mlEmilio Jesus Gallego Arias
2020-07-08Merge PR #12645: Cleanup Evarutil APIEmilio Jesus Gallego Arias
2020-07-08Merge PR #12652: Fix erroneous implicits-in-term warningEmilio Jesus Gallego Arias
2020-07-08Preserve delta-resolver at Module and Module Type starting.Hugo Herbelin
2020-07-08Remove Evarutil.new_evar_instance from the API.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_evar_from_context from the API.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_pure_evar_full from the API.Pierre-Marie Pédrot
2020-07-08Small code simplification in Evarutil.new_evar.Pierre-Marie Pédrot
2020-07-07Merge PR #12626: Fix Context with nonmaximplicit.Emilio Jesus Gallego Arias
2020-07-07Reindent ppvernac.mlGaëtan Gilbert
2020-07-07Fix erroneous implicits-in-term warningGaëtan Gilbert
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-05Fix Canonical with universe polymorphism and primitive projectionGaëtan Gilbert
2020-07-05Merge PR #12641: Windows build: use architecture dependent version of windresEnrico Tassi
2020-07-05Defined arbitrary base logarithms (Rlog) and added natural lemmas concerning ...Larry D. Lee Jr
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 09:48:44 +0000