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 /pretyping/vnorm.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 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 1420401875..314cada2d7 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -287,7 +287,7 @@ and nf_stk ?from:(from=0) env sigma c t stk = CaseInvert {univs=u; args=allargs} else NoInvert in - nf_stk env sigma (mkCase(ci, p, iv, c, branchs)) tcase stk + nf_stk env sigma (mkCase (Inductive.contract_case env (ci, p, iv, c, branchs))) tcase stk | Zproj p :: stk -> assert (from = 0) ; let p' = Projection.make p true in |