Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
use rec( ("$1") := 2 ) instead of rec( $1 := 2 )
as the latter does not work anymore From: Alexander Konovalov <alexk@mcs.st-andrews.ac.uk> Subject: $ in identifiers Date: 4. Februar 2014 23:37:32 MEZ To: Mohamed Barakat <mohamed.barakat@rwth-aachen.de> Dear Mohamed, sorry for not reporting this before: actually, dollar is no longer allowed in identifiers. Would it be possible to fix this in GradedRingForHomalg? ...
- Loading branch information