From a1fb276dbc976feb25dce396074fd996285f8686 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 4 Jan 2017 09:52:51 +0100
Subject: [PATCH] A bit more syntactic sugar. More proof rules for letcall,
letalloc.
---
opam.pins | 2 +-
theories/lang/lang.v | 24 ++++++++++++
theories/lang/memcpy.v | 5 ++-
theories/lang/new_delete.v | 12 +++++-
theories/lang/notation.v | 63 ++++++++++++++++---------------
theories/lang/tactics.v | 2 +-
theories/typing/cont.v | 4 +-
theories/typing/function.v | 40 +++++++++++++++++---
theories/typing/own.v | 68 +++++++++++++++++++++++++++++++---
theories/typing/product.v | 6 +--
theories/typing/sum.v | 6 +--
theories/typing/type_context.v | 10 ++---
12 files changed, 184 insertions(+), 58 deletions(-)
diff --git a/opam.pins b/opam.pins
index 3a65a2b9..f70be399 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq e0789039ed0dcb01b6249fec2d5a36f66e5de21c
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 53fe9f4028ceeb7346a528ad0748fd0f3de3edd5
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 62342edc..af91c92d 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -19,6 +19,13 @@ Inductive binder := BAnon | BNamed : string → binder.
Delimit Scope lrust_binder_scope with RustB.
Bind Scope lrust_binder_scope with binder.
+Notation "a :: b" := (@cons binder a%RustB b%RustB)
+ (at level 60, right associativity) : lrust_binder_scope.
+Notation "[ x1 ; x2 ; .. ; xn ]" :=
+ (@cons binder x1%RustB (@cons binder x2%RustB
+ (..(@cons binder xn%RustB (@nil binder))..))) : lrust_binder_scope.
+Notation "[ x ]" := (@cons binder x%RustB (@nil binder)) : lrust_binder_scope.
+
Definition cons_binder (mx : binder) (X : list string) : list string :=
match mx with BAnon => X | BNamed x => x :: X end.
Infix ":b:" := cons_binder (at level 60, right associativity).
@@ -477,6 +484,23 @@ Proof. intros. apply is_closed_subst with []; set_solver. Qed.
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
+Lemma subst_is_closed X x es e :
+ is_closed X es → is_closed (x::X) e → is_closed X (subst x es e).
+Proof.
+ revert e X. fix 1; destruct e=>X //=; repeat (case_bool_decide=>//=);
+ try naive_solver; rewrite ?andb_True; intros.
+ - set_solver.
+ - eauto using is_closed_weaken with set_solver.
+ - eapply is_closed_weaken; first done.
+ destruct (decide (BNamed x = f)), (decide (BNamed x ∈ xl)); set_solver.
+ - split; first naive_solver. induction el; naive_solver.
+ - split; first naive_solver. induction el; naive_solver.
+Qed.
+
+Lemma subst'_is_closed X b es e :
+ is_closed X es → is_closed (b:b:X) e → is_closed X (subst' b es e).
+Proof. destruct b; first done. apply subst_is_closed. Qed.
+
(* Operations on literals *)
Lemma lit_eq_state σ1 σ2 l1 l2 :
(∀ l, σ1 !! l = None ↔ σ2 !! l = None) →
diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index ca2fe83d..59c8c117 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -9,7 +9,10 @@ Definition memcpy : val :=
"memcpy" ["dst" +â‚— #1 ; "len" - #1 ; "src" +â‚— #1].
Global Opaque memcpy.
-Notation "e1 <-{ n } ! e2" := (App memcpy [e1%E ; Lit (LitInt n) ; e2%E])
+Notation "e1 <-{ n } ! e2" :=
+ (memcpy (@cons expr e1%E
+ (@cons expr (Lit n)
+ (@cons expr e2%E nil))))
(at level 80, n at next level, format "e1 <-{ n } ! e2") : expr_scope.
Notation "e1 <-[ i ]{ n } ! e2" :=
diff --git a/theories/lang/new_delete.v b/theories/lang/new_delete.v
index 66224fec..6318799b 100644
--- a/theories/lang/new_delete.v
+++ b/theories/lang/new_delete.v
@@ -1,6 +1,6 @@
From iris.base_logic.lib Require Import namespaces.
From lrust.lang Require Export notation.
-From lrust.lang Require Import heap proofmode.
+From lrust.lang Require Import heap proofmode memcpy.
Definition new : val :=
λ: ["n"],
@@ -38,4 +38,12 @@ Section specs.
iIntros (? ? Φ) "(#Hinv & H↦ & [H†|%]) HΦ";
wp_lam; wp_op; intros ?; try lia; wp_if; try wp_free; by iApply "HΦ".
Qed.
-End specs.
\ No newline at end of file
+End specs.
+
+(* FIXME : why are these notations not pretty-printed. *)
+Notation "'letalloc:' x := e1 'in' e2" :=
+ ((Lam (@cons binder x%E%E%E nil) (x <- e1 ;; e2)) [new [ #1]])%E
+ (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
+Notation "'letalloc:' x :={ n } ! e1 'in' e2" :=
+ ((Lam (@cons binder x%E%E%E nil) (x <-{ n%Z%V } ! e1 ;; e2)) [new [ #n]%E%E])%E
+ (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index af9528f2..176b7adb 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -36,45 +36,50 @@ Notation "e1 <-ˢᶜ e2" := (Write ScOrd e1%E e2%E)
(at level 80) : expr_scope.
Notation "e1 <- e2" := (Write Na1Ord e1%E e2%E)
(at level 80) : expr_scope.
-Notation "'rec:' f [ x1 ; .. ; xn ] := e" :=
- (Rec f%RustB ( @cons binder x1%RustB ( .. (@cons binder xn%RustB nil) ..)) e%E)
- (at level 102, f at level 1, x1 at level 1, xn at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f [ x1 ; .. ; xn ] := e" :=
- (RecV f%RustB ( @cons binder x1%RustB ( .. (@cons binder xn%RustB nil) ..)) e%E)
- (at level 102, f at level 1, x1 at level 1, xn at level 1, e at level 200) : val_scope.
-Notation "'rec:' f [ ] := e" := (Rec f%RustB nil e%E)
- (at level 102, f at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f [ ] := e" := (RecV f%RustB nil e%E)
- (at level 102, f at level 1, e at level 200) : val_scope.
+Notation "'rec:' f xl := e" := (Rec f%RustB xl%RustB e%E)
+ (at level 102, f, xl at level 1, e at level 200) : expr_scope.
+Notation "'rec:' f xl := e" := (RecV f%RustB xl%RustB e%E)
+ (at level 102, f, xl at level 1, e at level 200) : val_scope.
Notation "e1 +â‚— e2" := (BinOp OffsetOp e1%E e2%E)
(at level 50, left associativity) : expr_scope.
-(** Derived notions, in order of declaration. The notations for let and seq
-are stated explicitly instead of relying on the Notations Let and Seq as
-defined above. This is needed because App is now a coercion, and these
+(** Derived notions. The notations for let and seq are stated
+explicitly instead of relying on the Notations Let and Seq as defined
+above. This is needed because App is now a coercion, and these
notations are otherwise not pretty printed back accordingly. *)
-Notation "λ: [ x1 ; .. ; xn ] , e" :=
- (Lam ( @cons binder x1%RustB ( .. (@cons binder xn%RustB nil) ..)) e%E)
- (at level 102, x1 at level 1, xn at level 1, e at level 200) : expr_scope.
-Notation "λ: [ x1 ; .. ; xn ] , e" :=
- (LamV ( @cons binder x1%RustB ( .. (@cons binder xn%RustB nil) ..)) e%E)
- (at level 102, x1 at level 1, xn at level 1, e at level 200) : val_scope.
-Notation "λ: [ ] , e" := (Lam nil e%E)
- (at level 102, e at level 200) : expr_scope.
-Notation "λ: [ ] , e" := (LamV nil e%E)
- (at level 102, e at level 200) : val_scope.
-Notation "'let:' x := e1 'in' e2" := (Lam [x%RustB] e2%E [e1%E])
+Notation "λ: xl , e" := (Lam xl%RustB e%E)
+ (at level 102, xl at level 1, e at level 200) : expr_scope.
+Notation "λ: xl , e" := (LamV xl%RustB e%E)
+ (at level 102, xl at level 1, e at level 200) : val_scope.
+Notation "'funrec:' f xl → k := e" := (rec: f (k::xl) := e)%E
+ (only parsing, at level 102, f, xl at level 1, e at level 200) : expr_scope.
+Notation "'funrec:' f xl → k := e" := (rec: f (k::xl) := e)%V
+ (only parsing, at level 102, f, xl at level 1, e at level 200) : val_scope.
+
+Notation "'let:' x := e1 'in' e2" :=
+ ((Lam (@cons binder x%RustB nil) e2%E) (@cons expr e1%E nil))
(at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
-Notation "e1 ;; e2" := (Lam [BAnon] e2%E [e1%E])
+Notation "e1 ;; e2" := (let: <> := e1 in e2)%E
(at level 100, e2 at level 200, format "e1 ;; e2") : expr_scope.
(* These are not actually values, but we want them to be pretty-printed. *)
-Notation "'let:' x := e1 'in' e2" := (LamV [x%RustB] e2%E [e1%E])
+Notation "'let:' x := e1 'in' e2" :=
+ (LamV (@cons binder x%RustB nil) e2%E (@cons expr e1%E nil))
(at level 102, x at level 1, e1, e2 at level 200) : val_scope.
-Notation "e1 ;; e2" := (LamV [BAnon] e2%E [e1%E])
+Notation "e1 ;; e2" := (let: <> := e1 in e2)%V
(at level 100, e2 at level 200, format "e1 ;; e2") : val_scope.
+Notation "'letcont:' k xl := e1 'in' e2" :=
+ ((Lam (@cons binder k%RustB nil) e2%E) [Rec k%RustB xl%RustB e1%E])
+ (only parsing, at level 102, k, xl at level 1, e1, e2 at level 200) : expr_scope.
+
+Notation "'call:' f args → k" := (f (@cons expr k args))%E
+ (only parsing, at level 102, f, args, k at level 1) : expr_scope.
+Notation "'letcall:' x := f args 'in' e" :=
+ (letcont: "_k" [ x ] := e in call: f args → "_k")%E
+ (at level 102, x, f, args at level 1, e at level 200) : expr_scope.
+
Notation "e1 <-[ i ] '☇'" := (e1 <- #i)%E
(only parsing, at level 80) : expr_scope.
-Notation "e1 <-[ i ] e2" := (e1<-[i] ☇ ;; e1+ₗ#1 <- e2)%E
- (at level 80) : expr_scope.
+Notation "e1 <-[ i ] e2" := (e1 <-[i] ☇ ;; e1+ₗ#1 <- e2)%E
+ (at level 80) : expr_scope.
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index d19ef64e..bc8fd232 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -3,7 +3,7 @@ From lrust.lang Require Export lang.
(** We define an alternative representation of expressions in which the
embedding of values and closed expressions is explicit. By reification of
-expressions into this type we can implementation substitution, closedness
+expressions into this type we can implement substitution, closedness
checking, atomic checking, and conversion into values, by computation. *)
Module W.
Inductive expr :=
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index d708479f..99e45bab 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -19,12 +19,12 @@ Section typing.
rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "* Htl HL HT").
Qed.
- Lemma type_cont L1 {argsb} T' E L2 C T econt e2 kb :
+ Lemma type_cont argsb L1 T' E L2 C T econt e2 kb :
Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
(∀ k args, typed_body E L1 (k â—cont(L1, T') :: C) (T' args)
(subst_v (kb::argsb) (k:::args) econt)) →
(∀ k, typed_body E L2 (k â—cont(L1, T') :: C) T (subst' kb k e2)) →
- typed_body E L2 C T (let: kb := Rec kb argsb econt in e2).
+ typed_body E L2 C T (letcont: kb argsb := econt in e2).
Proof.
iIntros (Hc1 Hc2 Hecont He2 tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
{ simpl. rewrite decide_left. done. }
diff --git a/theories/typing/function.v b/theories/typing/function.v
index b3e5e533..b052b08f 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
From iris.algebra Require Import vector.
From lrust.lifetime Require Import borrow.
From lrust.typing Require Export type.
-From lrust.typing Require Import programs.
+From lrust.typing Require Import programs cont.
Section fn.
Context `{typeG Σ} {A : Type} {n : nat}.
@@ -140,11 +140,11 @@ Section typing.
(* TODO: Define some syntactic sugar for calling and letrec like we do on paper. *)
Lemma type_call {A} E L E' T p (ps : list path)
- (tys : A → vec type (length ps)) ty k x :
+ (tys : A → vec type (length ps)) ty k x :
elctx_sat E L (E' x) →
typed_body E L [k â—cont(L, λ v : vec _ 1, (v!!!0 â— ty x) :: T)]
((p â— fn E' tys ty) :: zip_with TCtx_hasty ps (tys x) ++ T)
- (p (of_val k :: ps)).
+ (call: p ps → k).
Proof.
iIntros (HE tid qE) "#HEAP #LFT Htl HE HL HC".
rewrite tctx_interp_cons tctx_interp_app. iIntros "(Hf & Hargs & HT)".
@@ -187,7 +187,7 @@ Section typing.
tctx_extract_ctx E L (zip_with TCtx_hasty ps (tys x)) T T' →
(k â—cont(L, T''))%CC ∈ C →
(∀ ret : val, tctx_incl E L ((ret ◠ty x)::T') (T'' [# ret])) →
- typed_body E L C T (p (of_val k :: ps)).
+ typed_body E L C T (call: p ps → k).
Proof.
intros Hfn HE HTT' HC HT'T''.
rewrite -typed_body_mono /flip; last done; first by eapply type_call.
@@ -197,6 +197,36 @@ Section typing.
apply copy_elem_of_tctx_incl; last done. apply _.
Qed.
+ Lemma type_letcall {A} x E L E' C T T' p (ps : list path)
+ (tys : A → vec type (length ps)) ty b e :
+ Closed (b :b: []) e → Closed [] p → Forall (Closed []) ps →
+ (p ◠fn E' tys ty)%TC ∈ T →
+ elctx_sat E L (E' x) →
+ tctx_extract_ctx E L (zip_with TCtx_hasty ps (tys x)) T T' →
+ (∀ ret : val, typed_body E L C ((ret ◠ty x)::T') (subst' b ret e)) →
+ typed_body E L C T (letcall: b := p ps in e).
+ Proof.
+ intros ?? Hpsc ????. eapply (type_cont [_] _ (λ r, (r!!!0 ◠ty x) :: T')%TC).
+ - (* TODO : make [solve_closed] work here. *)
+ eapply is_closed_weaken; first done. set_solver+.
+ - (* TODO : make [solve_closed] work here. *)
+ rewrite /Closed /= !andb_True. split.
+ + by eapply is_closed_weaken, list_subseteq_nil.
+ + eapply Is_true_eq_left, forallb_forall, List.Forall_forall, Forall_impl=>//.
+ intros. eapply Is_true_eq_true, is_closed_weaken=>//. set_solver+.
+ - intros k ret. inv_vec ret=>ret v0. inv_vec v0. rewrite /subst_v /=.
+ rewrite ->(is_closed_subst []), incl_cctx_incl; first done; try set_solver+.
+ apply subst'_is_closed; last done. apply is_closed_of_val.
+ - intros.
+ (* TODO : make [simpl_subst] work here. *)
+ change (subst' "_k" k (p (Var "_k" :: ps))) with
+ ((subst "_k" k p) (of_val k :: map (subst "_k" k) ps)).
+ rewrite is_closed_nil_subst //.
+ assert (map (subst "_k" k) ps = ps) as ->.
+ { clear -Hpsc. induction Hpsc=>//=. rewrite is_closed_nil_subst //. congruence. }
+ eapply type_call'; try done. constructor. done.
+ Qed.
+
Lemma type_fn {A} E L E' fb kb (argsb : list binder) e
(tys : A → vec type (length argsb)) ty
T `{!CopyC T, !SendC T} :
@@ -206,7 +236,7 @@ Section typing.
((f â— fn E' tys ty) ::
zip_with (TCtx_hasty ∘ of_val) args (tys x) ++ T)
(subst_v (fb :: kb :: argsb) (f ::: k ::: args) e)) →
- typed_instruction_ty E L T (Rec fb (kb :: argsb) e) (fn E' tys ty).
+ typed_instruction_ty E L T (funrec: fb argsb → kb := e) (fn E' tys ty).
Proof.
iIntros (Hc Hbody tid qE) "#HEAP #LFT $ $ $ #HT". iApply wp_value.
{ simpl. rewrite decide_left. done. }
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 8c5d5da0..256d7b41 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -3,6 +3,7 @@ From iris.proofmode Require Import tactics.
From iris.base_logic Require Import big_op.
From lrust.lifetime Require Import borrow frac_borrow.
From lrust.lang Require Export new_delete.
+From lrust.lang Require Import memcpy.
From lrust.typing Require Export type.
From lrust.typing Require Import uninit type_context programs.
@@ -159,8 +160,11 @@ Section typing.
Proof.
iIntros (Hsz p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
- rewrite ty'.(ty_size_eq). (* This turns out to be the fastest way to apply a lemma below â–· -- at least if we're fine throwing away the premise even though the result is persistent, which in this case, we are. *)
- iDestruct "Hown" as ">%". iModIntro. iExists _, _. iFrame "H↦".
+ (* This turns out to be the fastest way to apply a lemma below â–· -- at
+ least if we're fine throwing away the premise even though the result
+ is persistent, which in this case, we are. *)
+ rewrite ty'.(ty_size_eq). iDestruct "Hown" as ">%". iModIntro.
+ iExists _, _. iFrame "H↦".
iSplit; first by rewrite Hsz. iIntros "Hown !>".
iExists _. iSplit; first done. rewrite Hsz. iFrame.
Qed.
@@ -186,7 +190,7 @@ Section typing.
iFrame. iApply uninit_own. auto.
Qed.
- Lemma type_new E L (n : nat) :
+ Lemma type_new {E L} (n : nat) :
typed_instruction_ty E L [] (new [ #n ]%E) (own n (uninit n)).
Proof.
iIntros (tid eq) "#HEAP #LFT $ $ $ _".
@@ -201,11 +205,11 @@ Section typing.
- by rewrite uninit_sz freeable_sz_full.
Qed.
- Lemma type_delete E L n ty p :
- n = ty.(ty_size) →
+ Lemma type_delete {E L} ty n p :
+ ty.(ty_size) = n →
typed_instruction E L [p ◠own n ty] (delete [ #n; p])%E (λ _, []).
Proof.
- iIntros (-> tid eq) "#HEAP #LFT $ $ $ Hp". rewrite tctx_interp_singleton.
+ iIntros (<- tid eq) "#HEAP #LFT $ $ $ Hp". rewrite tctx_interp_singleton.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
iDestruct "Hown" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
iDestruct "H↦∗:" as (vl) "[>H↦ Hown]". rewrite tctx_interp_nil.
@@ -213,6 +217,58 @@ Section typing.
iApply (wp_delete with "[-]"); try (by auto); [].
rewrite freeable_sz_full. by iFrame.
Qed.
+
+ Lemma type_letalloc_1 {E L} ty C T T' (x : string) p e :
+ ty.(ty_size) = 1%nat →
+ Closed [] p → Closed (x :b: []) e →
+ tctx_extract_hasty E L p ty T T' →
+ (∀ v, typed_body E L C ((v ◠own 1 ty)::T') (subst x v e)) →
+ typed_body E L C T (letalloc: x := p in e).
+ Proof.
+ intros. eapply type_let'.
+ - rewrite /Closed /=. rewrite !andb_True.
+ eauto 10 using is_closed_weaken with set_solver.
+ - apply (type_new 1).
+ - solve_typing.
+ - move=>xv /=.
+ assert (subst x xv (x <- p ;; e)%E = (xv <- p ;; subst x xv e)%E) as ->.
+ { (* TODO : simpl_subst should be able to do this. *)
+ unfold subst=>/=. repeat f_equal.
+ - by rewrite bool_decide_true.
+ - eapply is_closed_subst. done. set_solver. }
+ eapply type_let'.
+ + apply subst_is_closed; last done. apply is_closed_of_val.
+ + by apply (type_assign ty (own 1 (uninit 1))), write_own.
+ + solve_typing.
+ + move=>//=.
+ Qed.
+
+ Lemma type_letalloc_n {E L} ty ty1 ty2 C T T' (x : string) p e :
+ Closed [] p → Closed (x :b: []) e →
+ typed_read E L ty1 ty ty2 →
+ tctx_extract_hasty E L p ty1 T T' →
+ (∀ v, typed_body E L C ((v ◠own (ty.(ty_size)) ty)::(p ◠ty2)::T') (subst x v e)) →
+ typed_body E L C T (letalloc: x :={ty.(ty_size)} !p in e).
+ Proof.
+ intros. eapply type_let'.
+ - rewrite /Closed /=. rewrite !andb_True.
+ eauto 100 using is_closed_weaken with set_solver.
+ - apply type_new.
+ - solve_typing.
+ - move=>xv /=.
+ assert (subst x xv (x <-{ty.(ty_size)} !p ;; e)%E =
+ (xv <-{ty.(ty_size)} !p ;; subst x xv e)%E) as ->.
+ { (* TODO : simpl_subst should be able to do this. *)
+ unfold subst=>/=. repeat f_equal.
+ - eapply (is_closed_subst []). done. set_solver.
+ - by rewrite bool_decide_true.
+ - eapply is_closed_subst. done. set_solver. }
+ eapply type_let'.
+ + apply subst_is_closed; last done. apply is_closed_of_val.
+ + eapply type_memcpy; try done. apply write_own, symmetry, uninit_sz.
+ + solve_typing.
+ + move=>//=.
+ Qed.
End typing.
Hint Resolve own_mono' own_proper' : lrust_typing.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index b83e10de..dbb855ff 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -245,6 +245,6 @@ Section typing.
End typing.
-Hint Resolve product_mono' product_proper' : lrust_type_scope.
-Hint Constructors Forall2 : lrust_type_scope.
-Hint Resolve product2_mono' product2_proper' | 100 : lrust_type_scope.
+Hint Resolve product_mono' product_proper' : lrust_typing.
+Hint Constructors Forall2 : lrust_typing.
+Hint Resolve product2_mono' product2_proper' | 100 : lrust_typing.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index a60c01d1..79bee07a 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -235,7 +235,7 @@ End sum.
(* Σ is commonly used for the current functor. So it cannot be defined
as Î for products. We stick to the following form. *)
Notation "Σ[ ty1 ; .. ; tyn ]" :=
- (sum (cons ty1 (..(cons tyn nil)..))) : lrust_type_scope.
+ (sum (cons ty1 (..(cons tyn nil)..))) : lrust_typing.
-Hint Resolve sum_mono' sum_proper' : lrust_type_scope.
-Hint Constructors Forall2 : lrust_type_scope.
+Hint Resolve sum_mono' sum_proper' : lrust_typing.
+Hint Constructors Forall2 : lrust_typing.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index f7d7159e..33596b8e 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -321,10 +321,10 @@ Section type_context.
Qed.
End type_context.
-Hint Resolve tctx_extract_hasty_here_copy : lrust_tctx_scope.
-Hint Resolve tctx_extract_hasty_here | 50 : lrust_tctx_scope.
-Hint Resolve tctx_extract_hasty_cons | 100 : lrust_tctx_scope.
-Hint Extern 1 (Copy _) => typeclasses eauto : lrust_tctx_scope.
+Hint Resolve tctx_extract_hasty_here_copy : lrust_typing.
+Hint Resolve tctx_extract_hasty_here | 50 : lrust_typing.
+Hint Resolve tctx_extract_hasty_cons | 100 : lrust_typing.
+Hint Extern 1 (Copy _) => typeclasses eauto : lrust_typing.
Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons
tctx_extract_ctx_nil tctx_extract_ctx_hasty
- tctx_extract_ctx_blocked tctx_extract_ctx_incl : lrust_tctx_scope.
+ tctx_extract_ctx_blocked tctx_extract_ctx_incl : lrust_typing.
--
GitLab