[ fix ] --rewriting is infective

gallais · gallais · commit df978c6ad7b9 · 2021-02-08T14:55:39.000Z
Following agda/agda#4621, --rewriting is infective
diff --git a/GenerateEverything.hs b/GenerateEverything.hs
@@ -235,6 +235,7 @@ main = do
 
   writeFileUTF8 (allOutputFile ++ ".agda") $
     unlines [ header
+            , "{-# OPTIONS --rewriting #-}\n"
             , mkModule allOutputFile
             , format libraryfiles
             ]
diff --git a/Header b/Header
@@ -5,4 +5,3 @@
 ------------------------------------------------------------------------
 
 -- Note that core modules are not included.
-
diff --git a/README.agda b/README.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --rewriting #-}
+
 module README where
 
 ------------------------------------------------------------------------
diff --git a/README/Debug/Trace.agda b/README/Debug/Trace.agda
@@ -4,7 +4,7 @@
 -- An example showing how the Debug.Trace module can be used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K #-}
+{-# OPTIONS --without-K --rewriting #-}
 
 module README.Debug.Trace where
 

Original file line number	Diff line number	Diff line change
`@@ -235,6 +235,7 @@ main = do`
`235`	`235`
`236`	`236`	`writeFileUTF8 (allOutputFile ++ ".agda") $`
`237`	`237`	`unlines [ header`
	`238`	`+ , "{-# OPTIONS --rewriting #-}\n"`
`238`	`239`	`, mkModule allOutputFile`
`239`	`240`	`, format libraryfiles`
`240`	`241`	`]`
Original file line number	Diff line number	Diff line change
`@@ -5,4 +5,3 @@`
`5`	`5`	`------------------------------------------------------------------------`
`6`	`6`
`7`	`7`	`-- Note that core modules are not included.`
`8`		`-`