From 18880888d56b3f5f1e69ddadb7aadf02b0c56401 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 12 Jun 2018 11:35:08 +0200 Subject: Test file for #7723 --- kernel/cbytegen.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'kernel') diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 1b909a8d0..f17313230 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -258,14 +258,12 @@ let pos_universe_var i r sz = (* Compilation of a universe variable can happen either at toplevel (the current closure correspond to a constant and has local universes) or in a local closure (which has no local universes). *) - if r.nb_uni_stack != 0 then begin + if r.nb_uni_stack != 0 then (* Universe variables are represented by De Bruijn levels (not indices), starting at 0. The shape of the stack will be [v1|..|vn|u1..up|arg1..argq] with size = n + p + q, and q = r.arity. So Kacc (sz - r.arity - 1) will access the last universe. *) - Printf.eprintf "pos_univ i=%i sz=%i arity=%i nb_univ=%i\n" i sz r.arity r.nb_uni_stack; Kacc (sz - r.arity - (r.nb_uni_stack - i)) - end else let env = !(r.in_env) in let db = FVuniv_var i in -- cgit v1.2.3