diff options
| author | Pierre-Marie Pédrot | 2018-04-09 13:20:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-11 13:09:03 +0200 |
| commit | 2f2d31d8408b4e15b193110309c4800a456cfb83 (patch) | |
| tree | 2acf7211d63835eee3bdf3063befe330e9dad3e3 /kernel/reduction.ml | |
| parent | 4a244648cff78c7f7333ac5b335de3f6e742908a (diff) | |
The cbv reduction does not rely on the kernel info data structure anymore.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 00576476ab..18697d07e5 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -316,8 +316,8 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = type conv_tab = { cnv_inf : clos_infos; - lft_tab : fconstr infos_tab; - rgt_tab : fconstr infos_tab; + lft_tab : clos_tab; + rgt_tab : clos_tab; } (** Invariant: for any tl ∈ lft_tab and tr ∈ rgt_tab, there is no mutable memory location contained both in tl and in tr. *) @@ -346,7 +346,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (Sort s1, Sort s2) -> if not (is_empty_stack v1 && is_empty_stack v2) then anomaly (Pp.str "conversion was given ill-typed terms (Sort)."); - sort_cmp_universes (env_of_infos infos.cnv_inf) cv_pb s1 s2 cuniv + sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv | (Meta n, Meta m) -> if Int.equal n m then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv |