diff options
| author | Maxime Dénès | 2018-09-14 17:42:54 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-17 09:33:30 +0200 |
| commit | a8bf1cab3f21de4a350737ef5c933af1746f54a1 (patch) | |
| tree | 65c726bd3576603c273c772bf1b22e36d07f898a /pretyping | |
| parent | 42706b1cd101f389f3e704f859200a35316bd97e (diff) | |
OCaml now exports the min and max non-constant tags, let's use it
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/vnorm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 59e60aa8f4..82c732c59f 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -161,9 +161,9 @@ and nf_whd env sigma whd typ = | Vconstr_block b -> let tag = btag b in let (tag,ofs) = - if tag = last_variant_tag then + if tag = Obj.last_non_constant_constructor_tag then match whd_val (bfield b 0) with - | Vconstr_const tag -> (tag+last_variant_tag, 1) + | Vconstr_const tag -> (tag+Obj.last_non_constant_constructor_tag, 1) | _ -> assert false else (tag, 0) in let capp,ctyp = construct_of_constr_block env tag typ in |