diff options
| author | Matej Kosik | 2015-10-29 14:42:15 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:09 +0100 |
| commit | 9f6ca170331a4f883cae20531bdced9eee663c59 (patch) | |
| tree | 0a605f4200a6b2173bb8f9813daa97caae1113ac | |
| parent | 0a5ee78c32b5f48d8f90de1ff073e250db5033d6 (diff) | |
CLEANUP PROPOSITION: removal of a definition of a concept that is not used further in the text
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 3 |
1 files changed, 0 insertions, 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$. |