From 9f77d69dcfcf4a36a400044ebd268a7d8d48e923 Mon Sep 17 00:00:00 2001 From: mueck Date: Thu, 2 Nov 2023 20:54:02 +0100 Subject: [PATCH] Minor improvement --- theories/type_systems/stlc_extended/bigstep.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/theories/type_systems/stlc_extended/bigstep.v b/theories/type_systems/stlc_extended/bigstep.v index eb5a78c..372f3d4 100644 --- a/theories/type_systems/stlc_extended/bigstep.v +++ b/theories/type_systems/stlc_extended/bigstep.v @@ -1,14 +1,12 @@ From stdpp Require Import gmap base relations. From iris Require Import prelude. -From semantics.ts.stlc_extended Require Import lang notation types. +From semantics.ts.stlc_extended Require Import lang notation. (** * Big-step semantics *) Implicit Types - (Γ : typing_context) (v : val) - (e : expr) - (A : type). + (e : expr). Inductive big_step : expr → val → Prop := | bs_lit (n : Z) :