Activity for RODIN
-
Guillaume Verdier created ticket #412
Automatic proof of inequality of datatype constructor with its arguments
-
Manual rewriter for arithmetic on constants
-
Overflow of description in tactic profile editor
-
RODIN released /Core_Rodin_Platform/3.10-RC1/README.md
-
-
-
-
-
-
better type synthesis for datatype
-
These changes have been merged in commit [df38cb].
-
Laurent Voisin committed [e77791] on RodinCore
Refactor DatatypeTranslator
-
Use isBasic of datatypes
-
Add method isBasic to datatypes
-
Optimize DatatypeBuilder
-
Add specialized shiftBoundIdentifiers
-
Remove useless method toTrgExpr
-
Rework makeSetConstructorFixpointAxiom
-
Rework makeSetConstructorUnionAxiom
-
Create TranslatingSetSubstitution
-
Add specialized translate method
-
Pass the extension rather than a source expression
-
Check target children rather than source
-
Extract methods mSetBID(s)
-
Extract methods mSetBoundIdent(s)
-
Make more precise the type of formulaRewriter
-
Make more precise the type of srcTypeConstructor
-
Remove hasDestructors
-
Avoid full recursive call
-
Use more precise array type
-
Extract mTrgFunImage
-
Change method name
-
Rename method
-
Document the source conversion
-
Document the source conversion
-
Automatic renaming of element in extension point
-
Fix FR#291 better type synthesis for datatype
-
Fix FR#291 better type synthesis for datatype
-
Extract method inferResultType
-
This has been implemented for destructors (where we already have the full type instantiation of the datatype. This has also been implemented on constructors when there is no type parameter.
-
More automatic proofs about finiteness
-
These cases have been implemented and merged in commit [3fc052].
-
Avoid startup error when external provers timeout
-
It has been implemented in commit [fc1669].
-
Pattern matching in ae
-
It has been implemented and merged in commit [1048bd].
-
Prepare Rodin 3.10
-
updating parent and plugins versions to 3.10
-
updating the year of the splash image
-
updating the year of the feature files
-
Rename the org.hamcrest plugin
-
upgrading to the new version of Eclipse (4.34)
-
upgrading from Tycho 4.0.3 to Tycho 4.0.9 required to build 4.34 products for Mac
-
Fix FR #410: More automatic proofs about finiteness
-
Extend FiniteInclusionTac to discharge finiteness of union
-
Extend FiniteInclusionTac to discharge finiteness of intersection
-
Extend FiniteInclusionTac to discharge finite(A) |- finite(A \ B)
-
Fix FR #409: Avoid startup error when external provers timeout
-
Fix bug introduced when fixing bug #835 and clean up ProofControlPage
-
Make private method out of duplicated code in ProofControlPage
-
Fix bug introduced when fixing bug #835
-
Fix FR #407: Pattern matching in ae
-
Extend ae with pattern "constructor(...)=expr"
-
Extend ae with pattern matching of maplets
-
Extend ae to handle multiple identifiers in left-hand-side of input
-
Extend deserialization of ae's input to allow multiple added identifiers
-
Simplify AbstrExprTests: pass type environment as string
-
Change handling of ae's input and its serialization
-
Fix typo (anticident to antecedent)
-
Impossible to type some datatype constructors
-
This has been fixed by Laurent Voisin and the fix was merged in commit [d90be2].
-
Fix bug #834: Impossible to type some datatype constructors
-
Test result of toStringWithTypes
-
Fix bug #834: Impossible to type some datatype constructors
-
Improve toStringWithTypes
-
Add needsTypeAnnotation to some test extensions
-
Add needsTypeAnnotation to TypeConstructorExtension
-
Add needsTypeAnnotation to DestructorExtension
-
Add needsTypeAnnotation to ConstructorExtension
-
Start implementing needsTypeAnnotation
-
Add needsTypeAnnotation method
-
Add tests about generic extension operators
-
Avoid spurious error in oftype annotations
-
Allow oftype for any extended expression
-
Rename method
-
Use type annotations
-
Start adding type annotation to extended expressions
-
Fix free identifiers for failing typecheck
-
Fix IdentsChecker
-
Refactor set extension
-
Simplify code in set extension
-
Add casts for signature resolution
-
Publish test extensions
-
Add some extensions for testing oftype annotations
-
Fix method typeCheck in CProd extension
-
Fix type-check methods of FIN extension
-
Strengthen datatypes
-
Check type parameters are used
-
Use type parameter in tests
-
Use all type parameters in tests
