Merge pull request #594 from XiaohuWang0921/master

Delete --guardedness flag
agda · Sep 20, 2021 · 6873f95 · 6873f95
2 parents 11ccf57 + 7078258
commit 6873f95
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/Cubical/Talks/EPA2020.agda b/Cubical/Talks/EPA2020.agda
@@ -12,8 +12,9 @@ Link to video: https://vimeo.com/459020971
 
 -}
 
--- To make Agda cubical add the following options
-{-# OPTIONS --safe --guardedness #-}
+-- To make Agda cubical add the --cubical option.
+-- This is implicitly added for files in the cubical library via the cubical.agda-lib file.
+{-# OPTIONS --safe #-}
 module Cubical.Talks.EPA2020 where
 
 -- The "Foundations" package contain a lot of important results (in

diff --git a/Everythings.hs b/Everythings.hs
@@ -85,7 +85,7 @@ genEverythings =
   mapM_ (\dir -> do
     let fp = addToFP ["Cubical"] dir
     files <- getMissingFiles fp Nothing
-    let ls = ["{-# OPTIONS --safe --guardedness #-}",
+    let ls = ["{-# OPTIONS --safe #-}",
               "module " ++ showFP '.' (addToFP fp "Everything") ++ " where",[]]
              ++ sort (fmap (\file -> "import " ++ showFP '.' file)
                            (delete (addToFP fp "Everything") files))