From 30fe571a398a0c71fb176b578a47e021a0ba63d6 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Sat, 21 Sep 2024 12:33:10 +0200 Subject: [PATCH] open scopes locally --- coq/equiv_debruijn.v | 4 ++-- coq/subtype_debruijn.v | 2 ++ 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/coq/equiv_debruijn.v b/coq/equiv_debruijn.v index 8d7f3cf..a905598 100644 --- a/coq/equiv_debruijn.v +++ b/coq/equiv_debruijn.v @@ -1,7 +1,7 @@ Require Import terms_debruijn. -Open Scope ladder_type_scope. -Open Scope ladder_expr_scope. +Local Open Scope ladder_type_scope. +Local Open Scope ladder_expr_scope. Create HintDb type_eq_hints. diff --git a/coq/subtype_debruijn.v b/coq/subtype_debruijn.v index 4fe2ed0..caedc58 100644 --- a/coq/subtype_debruijn.v +++ b/coq/subtype_debruijn.v @@ -18,6 +18,8 @@ Create HintDb subtype_hints. Reserved Notation "s ':<=' t" (at level 50). Reserved Notation "s '~<=' t" (at level 50). +Local Open Scope ladder_type_scope. + (* Representational Subtype *) Inductive is_repr_subtype : type_DeBruijn -> type_DeBruijn -> Prop := | TSubRepr_Refl : forall t t', (t === t') -> (t :<= t')