diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-12 11:35:08 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-27 13:28:01 +0200 |
| commit | 18880888d56b3f5f1e69ddadb7aadf02b0c56401 (patch) | |
| tree | 78db7878b0715491bff1c230ce0d2a140f722897 /kernel | |
| parent | ab84e2f45e2cdf99e5c69b90b628ef6618fe880a (diff) | |
Test file for #7723
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cbytegen.ml | 4 |
1 files changed, 1 insertions, 3 deletions
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 |