[Agda] Vezzosi's patch

[Sergei Meshveliani]

Wolfram wrote recently

> Have you tried this with Andrea Vezzosi's patch from
> https://github.com/agda/agda/issues/1625#issuecomment-132196576


I have looked there. This patch is about 
  src/full/Agda/TypeChecking/Conversion.hs

I have  Development Agda of March 21, 2017  (ghc-7.10.2, Debian Linux)
And the patch is probably the difference file for some old Agda.
Is this all right?
 
Well, I named the patch  V.diff  and commanded

  > mv V.diff  src/full/Agda/TypeChecking/

  > cd src/full/Agda/TypeChecking

  > patch Conversion.hs < V.diff

It reports that this point is found, and issues  Conversion.hs
with is about 500 byte longer.

Is this a correct way to use this patch?

Then, I install the obtained Agda, and install the standard library.
Then I type-check my application. 
But its error report is different. The original Agda succeeds, and the
patched Agda first type-checks several files and then reports something
like a wrong type in a certain .agda file.

I wonder, how to use this patch.

Thanks,

------
Sergei