From caecc75ed34fc00ff7ab8865873d7c23822fb902 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 7 Mar 2017 16:33:42 +0100
Subject: [PATCH] add typing.base; declare solve_typing and its DBs there
---
_CoqProject | 1 +
theories/typing/base.v | 14 ++++++++++++++
theories/typing/lft_contexts.v | 14 +-------------
theories/typing/type.v | 1 +
4 files changed, 17 insertions(+), 13 deletions(-)
create mode 100644 theories/typing/base.v
diff --git a/_CoqProject b/_CoqProject
index e334a62d..5cd928c7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -24,6 +24,7 @@ theories/lang/proofmode.v
theories/lang/races.v
theories/lang/tactics.v
theories/lang/spawn.v
+theories/typing/base.v
theories/typing/type.v
theories/typing/util.v
theories/typing/lft_contexts.v
diff --git a/theories/typing/base.v b/theories/typing/base.v
new file mode 100644
index 00000000..913b772e
--- /dev/null
+++ b/theories/typing/base.v
@@ -0,0 +1,14 @@
+From lrust.lifetime Require Export frac_borrow.
+
+Create HintDb lrust_typing.
+Create HintDb lrust_typing_merge.
+
+(* We first try to solve everything without the merging rules, and
+ then start from scratch with them.
+
+ The reason is that we want we want the search proof search for
+ [tctx_extract_hasty] to suceed even if the type is an evar, and
+ merging makes it diverge in this case. *)
+Ltac solve_typing :=
+ (typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
+ (typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 9ee1956b..dce104cb 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -2,6 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import fractional.
From lrust.lang Require Import proofmode.
+From lrust.typing Require Export base.
From lrust.lifetime Require Import frac_borrow.
Set Default Proof Using "Type".
@@ -453,19 +454,6 @@ End elctx_incl.
Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL.
-Create HintDb lrust_typing.
-Create HintDb lrust_typing_merge.
-
-(* We first try to solve everything without the merging rules, and
- then start from scratch with them.
-
- The reason is that we want we want the search proof search for
- [tctx_extract_hasty] to suceed even if the type is an evar, and
- merging makes it diverge in this case. *)
-Ltac solve_typing :=
- (typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
- (typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
-
Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
Hint Resolve of_val_unlock : lrust_typing.
Hint Resolve
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 706f7b2c..94219da4 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -2,6 +2,7 @@ From iris.base_logic.lib Require Export na_invariants.
From iris.base_logic Require Import big_op.
From lrust.lang Require Export proofmode notation.
From lrust.lifetime Require Export frac_borrow.
+From lrust.typing Require Export base.
From lrust.typing Require Import lft_contexts.
Set Default Proof Using "Type".
--
GitLab