Commit 3722288d authored by Michael Sammler's avatar Michael Sammler
Browse files

make lang.base depend on lithium.base

parent ebf59ae4
Pipeline #44700 passed with stage
in 32 minutes and 8 seconds
This diff is collapsed.
......@@ -2,4 +2,5 @@
(name refinedc.lang)
(package refinedc)
(flags -w -notation-overridden -w -redundant-canonical-projection)
(synopsis "Core language"))
(synopsis "Core language")
(theories refinedc.lithium))
This diff is collapsed.
(** Main typeclasses of Lithium *)
From iris.base_logic.lib Require Export iprop.
From iris.proofmode Require Export tactics.
From refinedc.lithium Require Import base infrastructure.
(** * [iProp_to_Prop] *)
......
......@@ -2,5 +2,4 @@
(name refinedc.lithium)
(package refinedc)
(flags -w -notation-overridden -w -redundant-canonical-projection)
(synopsis "Lithium")
(theories refinedc.lang))
(synopsis "Lithium"))
From refinedc.lang Require Export proofmode.
From refinedc.lithium Require Export lithium.
From refinedc.lang Require Export proofmode.
Create HintDb refinedc_typing.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment