diff options
| author | Vincent Laporte | 2018-09-07 11:18:28 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-14 07:51:12 +0000 |
| commit | 4be2dd481c783bed7c09086b647d860e42b7ea9f (patch) | |
| tree | dfd9a32619175eedb084915ed53d56c356d55174 /kernel/environ.ml | |
| parent | 38be62b56799933cdfc783d4e538963c3aa59fef (diff) | |
Retroknowledge.KInt31: remove the (unused) group parameter
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index e7efa5e2c9..64c93a2607 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -695,10 +695,10 @@ let register_one env field entry = (* [register env field entry] may register several fields when needed *) let register env field entry = match field with - | KInt31 (grp, Int31Type) -> + | KInt31 Int31Type -> let i31c = match kind entry with | Ind i31t -> mkConstructUi (i31t, 1) | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") in - register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry + register_one (register_one env (KInt31 Int31Constructor) i31c) field entry | field -> register_one env field entry |