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/nativeconv.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'kernel/nativeconv.ml') diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 6c755290d..bfa982136 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -60,7 +60,12 @@ and conv_atom env pb lvl a1 a2 cu = if a1 == a2 then cu else match a1, a2 with - | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false + | Ameta (m1,_), Ameta (m2,_) -> + if Int.equal m1 m2 then cu else raise NotConvertible + | Aevar (ev1,_,args1), Aevar (ev2,_,args2) -> + if Evar.equal ev1 ev2 then + Array.fold_right2 (conv_val env CONV lvl) args1 args2 cu + else raise NotConvertible | Arel i1, Arel i2 -> if Int.equal i1 i2 then cu else raise NotConvertible | Aind (ind1,u1), Aind (ind2,u2) -> @@ -112,7 +117,7 @@ and conv_atom env pb lvl a1 a2 cu = else conv_accu env CONV lvl ac1 ac2 cu | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _ - | Aproj _, _ -> raise NotConvertible + | Aproj _, _ | Ameta _, _ | Aevar _, _ -> raise NotConvertible (* Precondition length t1 = length f1 = length f2 = length t2 *) and conv_fix env lvl t1 f1 t2 f2 cu = -- cgit v1.2.3