Repository navigation

All pull requests

Adapt to rocq-prover/rocq#22173 (Delay q <= Type using above_prop)
#320SkySkimmer opened Oct 16, 2026Contributor
Adapt gcd proofs to the structural prelude definition
#317thomas-lamiaux opened Oct 11, 2026Contributor
Reals: a constructive pi for the constructive Cauchy reals with a strong irrationality separation theorem (Leibniz series)
#316hy7pc8gfmf-dotcom opened Oct 9, 20265 of 6 tasks
6
Add escape-window separation engine for the constructive Cauchy reals
#313hy7pc8gfmf-dotcom opened Oct 6, 2026
2
Adapt to rocq-prover/rocq#22113 (Proof Using Clear Unused)
#276SkySkimmer opened Jun 10, 2026Contributor
Small Linting of the code base to have a tab of 2
#266thomas-lamiaux opened May 17, 2026Contributor
4
Add a Version file allowing to identify the stdlib version from Rocq
#263mattam82 opened May 11, 2026Member1 of 2 tasks
15
Adapt to tify (https://github.com/rocq-community/micromega-plugin/pull/1)
#251fajb opened Apr 1, 2026Contributor
15
remove goal-modifying uses of injection
#248andres-erbsen opened Mar 17, 2026Collaborator
Wellfounded/Inclusion.v add lemma for when the inclusion is partial
#238SkySkimmer opened Feb 18, 2026Contributor
3
Rewrite Vector using list and small inversions
#170andres-erbsen opened Jun 11, 2025Collaborator1 of 8 tasks
Run test-suite on Alpine CI
#169andres-erbsen opened Jun 9, 2025Collaborator
Deprecate Relation_definitions, remove from supported files
#162andres-erbsen opened Jun 3, 2025Collaborator3 of 4 tasks
1
use RelationClasses instead of Relations_1 in Sorting
#152andres-erbsen opened May 31, 2025Collaborator1 of 3 tasks
remove Heap, PermutEq, and PermutSetoid from Sorting
#151andres-erbsen opened May 31, 2025Collaborator1 of 3 tasks
4
memb and nodupb in ListDec.v
#132Villetaneuse opened Apr 14, 2025Contributor3 tasks
1
Subtraction in NatInt
#119Villetaneuse opened Mar 10, 2025Contributor3 tasks
3
Rify + lra solves Mixed Integer Programs
#110fajb opened Feb 24, 2025Contributor3 tasks

Navigation Menu

Repository navigation

All pull requests

Adapt to rocq-prover/rocq#22173 (Delay q <= Type using above_prop)

Adapt gcd proofs to the structural prelude definition

Reals: a constructive pi for the constructive Cauchy reals with a strong irrationality separation theorem (Leibniz series)

Add escape-window separation engine for the constructive Cauchy reals

Adapt to rocq-prover/rocq#22113 (Proof Using Clear Unused)

Small Linting of the code base to have a tab of 2

Add a Version file allowing to identify the stdlib version from Rocq

Adapt to tify (https://github.com/rocq-community/micromega-plugin/pull/1)

remove goal-modifying uses of `injection`

Wellfounded/Inclusion.v add lemma for when the inclusion is partial

Rewrite Vector using list and small inversions

Run test-suite on Alpine CI

Deprecate Relation_definitions, remove from supported files

use RelationClasses instead of Relations_1 in Sorting

remove Heap, PermutEq, and PermutSetoid from Sorting

memb and nodupb in ListDec.v

Subtraction in NatInt

Rify + lra solves Mixed Integer Programs

Pull requests