Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Sep 17, 2025

• Coq -> Rocq

  damien-pous

  committed
  a88f0f4

  Copy full SHA for a88f0f4

• simplified proof of leq_t'

  damien-pous

  committed
  f214eb5

  Copy full SHA for f214eb5

Commits on Mar 26, 2025

• metadata for software heritage

  damien-pous

  committed
  823b424

  Copy full SHA for 823b424

Commits on Sep 18, 2024

• v1.20 for Coq 8.20

  damien-pous

  committed
  09caaf1

  Copy full SHA for 09caaf1

Commits on Apr 23, 2024

• Adapt to coq/coq#18938 (EConstr.ERelevance)

  

  SkySkimmer

  authored and

  damien-pous

  committed
  421077f

  Copy full SHA for 421077f

Commits on Mar 18, 2024

• version 1.9, for Coq 8.19

  damien-pous

  committed
  fea6bb3

  Copy full SHA for fea6bb3

Commits on Dec 6, 2023

• linking the companion to the tower as defined in [tower.v]

  Show description for 17ba810
  damien-pous

  committed
  17ba810

  Copy full SHA for 17ba810

Commits on Oct 20, 2023

• adjust opam and CI for Coq master, no compatibility with 8.18 and earlier

  

  palmskog

  authored and

  damien-pous

  committed
  65d0207

  Copy full SHA for 65d0207

• adapt opam and ci for 8.16 to 8.18 compatibility

  

  palmskog

  authored and

  damien-pous

  committed
  b4af290

  Copy full SHA for b4af290

• CI for master and 8.18

  damien-pous

  committed
  786cb50

  Copy full SHA for 786cb50

• changelog and version compatibility for v1.8

  damien-pous

  committed
  606c3a3

  Copy full SHA for 606c3a3

• port to Coq 8.18 (was lost in previous merge)

  damien-pous

  committed
  264533b

  Copy full SHA for 264533b

Commits on Aug 3, 2023

• add hint mode for CompleteLattice class to avoid divergence

  Show description for 1bd00d0
  

  2 peopleauthored and

  damien-pous

  committed
  1bd00d0

  Copy full SHA for 1bd00d0

Commits on Jul 21, 2023

• add gfp_bchain instantiation of gfp_chain to tower

  

  palmskog

  authored and

  damien-pous

  committed
  54db0f6

  Copy full SHA for 54db0f6

Commits on Jul 13, 2023

• fixing docker badge in readme

  damien-pous

  committed
  5bfe8b0

  Copy full SHA for 5bfe8b0

• Merge pull request #11 from palmskog/add-coq-dev-ci

  Show description for a96b56b
  damien-pous

  authored
  a96b56b

  Copy full SHA for a96b56b

• add basic Docker-Coq-Action opam-based CI for Coq master, including README badge

  palmskog

  committed
  db7c574

  Copy full SHA for db7c574

• Merge branch '8.17'

  damien-pous

  committed
  9614ea3

  Copy full SHA for 9614ea3

• v1.7 release (tower-based reimplementation)

  damien-pous

  committed
  026968d

  Copy full SHA for 026968d

• make master compile with coq.dev (for addition to Coq's CI)

  damien-pous

  committed
  2172e0c

  Copy full SHA for 2172e0c

Commits on Apr 18, 2023

• update changelog + readme

  damien-pous

  committed
  b037632

  Copy full SHA for b037632

• added a module [all] to load the library appropriately

  damien-pous

  committed
  9054017

  Copy full SHA for 9054017

• prefix notation ` inside a module to make the lib compatible with [Program]

  damien-pous

  committed
  cb190d0

  Copy full SHA for cb190d0

• packaged the CompleteLattice class differently to avoid exponential behaviour

  damien-pous

  committed
  eae6926

  Copy full SHA for eae6926

Commits on Mar 23, 2023

• inf_closed_all

  damien-pous

  committed
  035e5c8

  Copy full SHA for 035e5c8

Commits on Dec 26, 2022

• updating internal comments in tactics.v

  damien-pous

  committed
  94a5465

  Copy full SHA for 94a5465

Commits on Dec 23, 2022

• cleaning plus backward compatibility

  damien-pous

  committed
  23f3f1d

  Copy full SHA for 23f3f1d

• tower-based tactics

  damien-pous

  committed
  10e1f79

  Copy full SHA for 10e1f79

Commits on Dec 21, 2022

• tactic helpers, need a type for chain elements

  damien-pous

  committed
  405ed71

  Copy full SHA for 405ed71

• reverted to more powerful sup in lattice.v, tower helpers in rel.v

  damien-pous

  committed
  68d7872

  Copy full SHA for 68d7872

• coinduction via the final chain and tower induction

  damien-pous

  committed
  caad236

  Copy full SHA for caad236

• moving [coinduction] to [companion]

  damien-pous

  committed
  6c4418f

  Copy full SHA for 6c4418f

• reworking lattice module (breaks rel.v)

  damien-pous

  committed
  217402a

  Copy full SHA for 217402a

Commits on Sep 8, 2022

• fixing local opam file

  damien-pous

  committed
  88ac13e

  Copy full SHA for 88ac13e

• v1.6 for Coq 8.16

  damien-pous

  committed
  5c9e6bd

  Copy full SHA for 5c9e6bd

Pagination

Previous

Next