From 859794e3c0e2555936e6e5c4de98541ecf92ebef Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Jul 2016 10:31:37 +0200
Subject: [PATCH] Remove old comment.

---
 heap_lang/lang.v | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index db52e285a..982d7f41b 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -34,13 +34,6 @@ Qed.
 
 Inductive expr :=
   (* Base lambda calculus *)
-      (* Var is the only place where the terms contain a proof. The fact that they
-       contain a proof at all is suboptimal, since this means two seeminlgy
-       convertible terms could differ in their proofs. However, this also has
-       some advantages:
-       * We can make the [X] an index, so we can do non-dependent match.
-       * In expr_weaken, we can push the proof all the way into Var, making
-         sure that proofs never block computation. *)
   | Var (x : string)
   | Rec (f x : binder) (e : expr)
   | App (e1 e2 : expr)
-- 
GitLab