-
Notifications
You must be signed in to change notification settings - Fork 3
Issues: coq-community/trocq
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Automated class inference fault when using Something isn't working
UI
User interface of the plugin
Trocq Use
bug
#32
opened Jan 23, 2024 by
ecranceMERCE
Predicate naming in constraint graph
documentation
Improvements or additions to documentation
invalid
This doesn't seem right
#31
opened Jan 19, 2024 by
ecranceMERCE
Duplicate code getting parametricity classes
documentation
Improvements or additions to documentation
invalid
This doesn't seem right
#30
opened Jan 19, 2024 by
ecranceMERCE
Adapt and use HB to generate Trocq relational structures
dependencies
Compatibility with other packages
enhancement
New feature or request
#28
opened Jan 18, 2024 by
CohenCyril
Control in the New feature or request
UI
User interface of the plugin
trocq
tactic
enhancement
#27
opened Jan 18, 2024 by
ecranceMERCE
Trocq command opening goals
enhancement
New feature or request
UI
User interface of the plugin
#26
opened Jan 18, 2024 by
ecranceMERCE
Trocq records for inductive types
enhancement
New feature or request
theory
Theoretical aspects of the plugin
#25
opened Jan 18, 2024 by
ecranceMERCE
Combinator creating full parametricity witnesses from individual record fields
enhancement
New feature or request
#24
opened Jan 18, 2024 by
ecranceMERCE
Syntactic parametricity class search
question
Further information is requested
#23
opened Jan 18, 2024 by
ecranceMERCE
Suspension in implementation of weakening
documentation
Improvements or additions to documentation
#22
opened Jan 18, 2024 by
ecranceMERCE
Interaction of the Further information is requested
trocq
tactic with Coq
question
#21
opened Jan 18, 2024 by
ecranceMERCE
Suboptimal subtyping relation?
question
Further information is requested
theory
Theoretical aspects of the plugin
#20
opened Jan 18, 2024 by
ecranceMERCE
Support Trakt-like declarations for goal pre-processing
enhancement
New feature or request
UI
User interface of the plugin
#7
opened Nov 20, 2023 by
palmskog
Depending on regular Coq-ELPI
dependencies
Compatibility with other packages
#4
opened Nov 13, 2023 by
palmskog
ProTip!
Adding no:label will show everything without a label.