Skip to content

Pull requests: GoelandProver/Goeland

New pull request New
10 Open 45 Closed
10 Open 45 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Improve formatting by using golines part:infrastructure The PR is on non-goéland code
#69 opened Feb 22, 2026 by jrosain Loading…
Stop ignoring negated conjecture in problems kind:fix The PR fixes a bug part:parsing Issue/PR on the parsing of problems
#68 opened Oct 8, 2025 by jrosain Loading…
1
@jcailler
Fix lambdapi output by updating it with the new printer system has:other-pr-dependency This PR cannot be merged before another PR (the maintainer should specify the dependency(ies)) kind:cleanup Refactoring or improvement of existing code kind:fix The PR fixes a bug needs:ci Needs a CI run before merging part:lambdapi-output
#67 opened Oct 8, 2025 by jrosain Loading…
@jcailler
Add IProof interface with a tree structure and add relevant adapter for []Search.ProofStruct has:other-pr-dependency This PR cannot be merged before another PR (the maintainer should specify the dependency(ies)) kind:enhancement New feature or upgrade of a previous one needs:ci Needs a CI run before merging part:proof-output About the vanilla proof output (in custom format)
#64 opened Sep 1, 2025 by jrosain Loading… 1.2
@jcailler
1
Fix (sc)tptp output when the problem file is in cnf kind:fix The PR fixes a bug part:plugins The PR is about plugin-related code
#61 opened Aug 25, 2025 by jcailler Loading… 1.2
@jrosain
8
Fix syntax error on Rocq output by using a better printing system has:other-pr-dependency This PR cannot be merged before another PR (the maintainer should specify the dependency(ies)) kind:cleanup Refactoring or improvement of existing code kind:enhancement New feature or upgrade of a previous one kind:fix The PR fixes a bug needs:ci Needs a CI run before merging part:rocq-output About the certified output in Rocq
#59 opened Jul 29, 2025 by jrosain Loading… 1.2
1
@jcailler
2
Remove PrintError API and always call to Fatal or Anomaly instead kind:cleanup Refactoring or improvement of existing code part:logging The PR/issue is about logging
#57 opened Jul 27, 2025 by jrosain Loading… 1.2
@jcailler
Major overhaul of the type system to manage typed proof search with an easier-to-maintain and less invasive API has:other-pr-dependency This PR cannot be merged before another PR (the maintainer should specify the dependency(ies)) kind:cleanup Refactoring or improvement of existing code kind:enhancement New feature or upgrade of a previous one kind:fix The PR fixes a bug part:proof-search The PR is about the proof-search algorithm part:typing The PR is about typed terms/the typing algorithm part:unification About the unification process of Goéland
#53 opened Jul 27, 2025 by jrosain Loading… 1.2
1
@jcailler
Cleanup: replace *FormList by Lib.List[Form] kind:cleanup Refactoring or improvement of existing code
#46 opened Jul 20, 2025 by jrosain Loading… 1.2
@jcailler
5
Update PR instructions in CONTRIBUTING.md kind:documentation Enhance or add documentation part:infrastructure The PR is on non-goéland code
#31 opened Jul 10, 2025 by jcailler Loading… 1.2
@jrosain
12
ProTip! Follow long discussions with comments:>50.