Commits · master · The Rocq Prover / The Rocq Prover · GitLab

Mentions légales du service

Snippets Groups Projects

GitLab upgrade completed. Current version is 17.11.4.

Jul 04, 2025
- Merge PR #20867: [coqbot] Adapt to https://github.com/rocq-prover/bot/pull/344 · 2b545786
  coqbot authored 1 day ago
  2b545786
- Merge PR #20642: Remove KerPair.SyntacticOrd · ef4ce787
  coqbot authored 1 day ago
  ef4ce787
- Merge PR #20780: Fix univpoly cs unification · 10c6a6f3
  coqbot authored 1 day ago
  10c6a6f3
- [coqbot] Adapt to https://github.com/rocq-prover/bot/pull/344 · fdff2809
  Pierre Roux authored 1 day ago
  
  fdff2809
- Merge PR #20864: Add more stable anchor names for sections. · 4eac47de
  coqbot authored 1 day ago
  4eac47de
- Merge PR #17876: Add gramlib support for non-associativity and for deactivating the recovery mode · ed67c980
  coqbot authored 1 day ago
  ed67c980
- [CI] Temporarily disactivate kami · 5d7b04dc
  Pierre Roux authored 1 day ago
  5d7b04dc
- [CI] Temporarily disactivate SF · e3c2fe37
  Pierre Roux authored 1 week ago
  e3c2fe37
- [Corelib] Adapt · c63f7ec7
  Pierre Roux authored 2 weeks ago
  
  c63f7ec7
- [test-suite] Adapt · 6cb82d39
  Pierre Roux authored 2 weeks ago
  
  6cb82d39
Jul 03, 2025
- [refman] Adapt · 187b33e2
  Pierre Roux authored 2 weeks ago
  
  187b33e2
- Make Ltac2 work without recovery mode · 30ab11c0
  Pierre Roux authored 2 weeks ago
  
  30ab11c0
- Gramlib: add support for no-associativity. · 17df5cad
  HERBELIN Hugo authored 2 weeks ago and Pierre Roux committed 1 day ago
  
  17df5cad
- Gramlib: warn when recovery mode is used. · 2436a091
  HERBELIN Hugo authored 1 year ago and Pierre Roux committed 1 day ago
  
  2436a091
- Gramlib: also turn continuation-based fallback optional. · 1a252b5a
  HERBELIN Hugo authored 1 year ago and Pierre Roux committed 1 day ago
  1a252b5a
- Gramlib: make recovering strategy of parsing engine optional. · 09aab350
  HERBELIN Hugo authored 1 year ago and Pierre Roux committed 1 day ago
  
  09aab350
- Gramlib: postponing recovery heuristics after other "normal" strategies failed. · e781eb1b
  HERBELIN Hugo authored 1 year ago and Pierre Roux committed 1 day ago
  e781eb1b
- Gramlib: slightly disentangling a recursivity between types. · 7f164b41
  HERBELIN Hugo authored 1 year ago and Pierre Roux committed 1 day ago
  
  7f164b41
- Merge PR #20857: Qualified names for custom entries · a7353590
  coqbot authored 1 day ago
  a7353590
- Merge PR #20861: CI stdlib_doc on edge instead of base · 9fba3471
  coqbot authored 1 day ago
  9fba3471
- Add more stable anchor names for sections. · 4e4c29fc
  ZIMMERMANN Theo authored 2 days ago
  
  4e4c29fc
- Merge PR #20862: Remove incorrect comment in 9.0 compat file · 2e7fcb4e
  coqbot authored 2 days ago
  2e7fcb4e
- Don't hardcode CustomName for custom entries in procq · 61390451
  Gaëtan Gilbert authored 2 days ago
  61390451
- Qualified names for custom entries · 9c52d1ca
  Gaëtan Gilbert authored 4 days ago
  9c52d1ca
- CI stdlib_doc on edge instead of base · 66037f9f
  Gaëtan Gilbert authored 2 days ago
  66037f9f
- Remove incorrect comment in 9.0 compat file · 0dc41a42
  Gaëtan Gilbert authored 2 days ago
  0dc41a42
- Remove KerPair.SyntacticOrd · 567895ab
  Gaëtan Gilbert authored 1 month ago
  567895ab
- Merge PR #20819: Add modules shallowly in kernel module finalizer. · 53078a2b
  coqbot authored 2 days ago
  53078a2b
- Merge PR #20858: Correctly declare functor bodies in subtyping checks. · 253f6963
  coqbot authored 2 days ago
  253f6963
- Fix bugs in canonical structure resolution in unification.ml in presence of univ poly · 75c7a33c
  Matthieu Sozeau authored 1 month ago
  75c7a33c
- Merge PR #19977: Improve discrimination of lambdas in typeclass search · 91142f08
  coqbot authored 2 days ago
  91142f08
- Merge PR #20799: Slightly simplify ltac2 goal_match_list grammar declaration · 3c8fb94b
  coqbot authored 2 days ago
  3c8fb94b
- Merge PR #20834: Printmod cleanup name generation a bit · a4ccc9b9
  coqbot authored 2 days ago
  a4ccc9b9
- Merge PR #20815: Fix css again after #20744 · c3d55153
  coqbot authored 2 days ago
  c3d55153
Jul 02, 2025
- Correctly declare functor bodies in subtyping checks. · facbff7b
  Pierre-Marie Pédrot authored 2 days ago
  facbff7b
- Add modules shallowly in kernel module finalizer. · 26b5e21d
  Pierre-Marie Pédrot authored 1 week ago
  26b5e21d
- Merge PR #20854: Fix test suite after parallel merge of #20813 and #20824 · 7aa1b222
  coqbot authored 3 days ago
  7aa1b222
- Merge PR #20844: Rocqify issue templates · 250f3b96
  coqbot authored 3 days ago
  250f3b96
- Merge PR #20814: ci-common don't use ci_dir · d8ef00a7
  coqbot authored 3 days ago
  d8ef00a7
- Merge PR #20836: Names: move set/map modules `KNset` -> `KerName.Set` etc · bae348a4
  coqbot authored 3 days ago
  bae348a4