diff options
| author | Pierre-Marie Pédrot | 2019-03-03 21:03:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:00:20 +0100 |
| commit | d72e5c154faeea1d55387bc8c039d97f63ebd1c4 (patch) | |
| tree | d7f3c292606e98d2c2891354398e8d406d4dc15c /kernel/nativecode.ml | |
| parent | 6632739f853e42e5828fbf603f7a3089a00f33f7 (diff) | |
Change the representation of kernel case.
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 09db29d222..c19b883e3d 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -2101,7 +2101,7 @@ let compile_deps env sigma prefix init t = | Proj (p,c) -> let init = compile_mind_deps env prefix init (Projection.mind p) in aux env lvl init c - | Case (ci, _p, _iv, _c, _ac) -> + | Case (ci, _u, _pms, _p, _iv, _c, _ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix init mind in fold_constr_with_binders succ (aux env) lvl init t |