From 9f6ca170331a4f883cae20531bdced9eee663c59 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 29 Oct 2015 14:42:15 +0100
Subject: CLEANUP PROPOSITION: removal of a definition of a concept that is not
 used further in the text

---
 doc/refman/RefMan-cic.tex | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index b0205b7e9e..73fd4a1182 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -255,9 +255,6 @@ notation $[]$ denotes the empty local context.
 % $|\Delta|$ for the length of the context $\Delta$, that is for the number
 % of declarations (assumptions or definitions) in $\Delta$.
 
-A variable $x$ is said to be free in $\Gamma$ if $\Gamma$ contains a
-declaration $y:T$ such that $x$ is free in $T$.
-
 \paragraph[Global environment.]{Global environment.\index{Global environment}}
 %Because we are manipulating global declarations (global constants and global
 %assumptions), we also need to consider a global environment $E$.
-- 
cgit v1.2.3