From d041f19a7274b6065ca3ef565f0d8b8be08ef0d7 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 30 Jan 2018 10:45:03 +0100
Subject: [native_compute] Fix handling of evars in conversion

---
 kernel/nativevalues.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/nativevalues.ml')

diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 95a8fc5a4c..3d47b1672e 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -61,7 +61,7 @@ type atom =
   | Acofixe of t array * t array * int * t
   | Aprod of Name.t * t * (t -> t)
   | Ameta of metavariable * t
-  | Aevar of existential * t
+  | Aevar of Evar.t * t * t array
   | Aproj of Constant.t * accumulator
 
 let accumulate_tag = 0
@@ -132,8 +132,8 @@ let mk_prod_accu s dom codom =
 let mk_meta_accu mv ty =
   mk_accu (Ameta (mv,ty))
 
-let mk_evar_accu ev ty =
-  mk_accu (Aevar (ev,ty))
+let mk_evar_accu ev ty args =
+  mk_accu (Aevar (ev,ty,args))
 
 let mk_proj_accu kn c = 
   mk_accu (Aproj (kn,c))
-- 
cgit v1.2.3