Automatic proof of inequality of datatype constructor with its arguments
Manual rewriter for arithmetic on constants
Overflow of description in tactic profile editor
better type synthesis for datatype
These changes have been merged in commit [df38cb].
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