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/pretyping.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/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 9dbded75ba..e86a8a28c9 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1043,7 +1043,7 @@ struct if not record then let f = it_mkLambda_or_LetIn f fsign in let ci = make_case_info !!env (ind_of_ind_type indt) rci LetStyle in - mkCase (ci, p, make_case_invert !!env indt ci, cj.uj_val,[|f|]) + mkCase (EConstr.contract_case !!env sigma (ci, p, make_case_invert !!env indt ci, cj.uj_val,[|f|])) else it_mkLambda_or_LetIn f fsign in (* Make dependencies from arity signature impossible *) @@ -1159,7 +1159,7 @@ struct let pred = nf_evar sigma pred in let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val pred in let ci = make_case_info !!env (fst ind) rci IfStyle in - mkCase (ci, pred, make_case_invert !!env indty ci, cj.uj_val, [|b1;b2|]) + mkCase (EConstr.contract_case !!env sigma (ci, pred, make_case_invert !!env indty ci, cj.uj_val, [|b1;b2|])) in let cj = { uj_val = v; uj_type = p } in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon |