From 6fbe3c850bac9cbdfa64dbdcca7bd60dc7862190 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 19 Oct 2016 14:46:25 +0200
Subject: More comments in VM.

---
 kernel/vconv.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/vconv.ml')

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 894f5296a8..74d956bef0 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -77,6 +77,7 @@ and conv_whd env pb k whd1 whd2 cu =
   | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) ->
       conv_atom env pb k a1 stk1 a2 stk2 cu
   | Vfun _, _ | _, Vfun _ ->
+     (* on the fly eta expansion *)
       conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu
 
   | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _  | Vconstr_const _, _
-- 
cgit v1.2.3