From ee9baa0d9cbf14b89e9fc8729104bea201673381 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Wed, 6 Jul 2016 14:12:32 +0200 Subject: [PATCH] Revert "Add notations in fundamental_unary for aesthetics" This reverts commit b498dbc475d6e53694be560120a769d5a759a208. --- F_mu_ref_conc/fundamental_unary.v | 3 --- 1 file changed, 3 deletions(-) diff --git a/F_mu_ref_conc/fundamental_unary.v b/F_mu_ref_conc/fundamental_unary.v index 681c6d8..248d9c9 100644 --- a/F_mu_ref_conc/fundamental_unary.v +++ b/F_mu_ref_conc/fundamental_unary.v @@ -19,9 +19,6 @@ Section typed_interp. Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|]. - Local Notation "A –≻ B" := (TArrow A B) (at level 200). - Local Notation "e < n - vs" := (e.[upn n (env_subst vs)]) (at level 200). - Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → Γ ⊨ e : τ. Proof. induction 1; iIntros {Δ vs HΔ} "#[Hheap HΓ] /=". -- GitLab