diff options
| author | Vincent Laporte | 2018-09-07 17:34:11 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-14 07:51:17 +0000 |
| commit | 2ec78477c720ba3a5343b49f25cfa9c1639adbba (patch) | |
| tree | ed8129ee7206bcb32c5e7d41830caf22b7cc2254 /kernel/environ.ml | |
| parent | 42bed627c4a1c5a1ecf59d4865fc872b5eee7290 (diff) | |
Retroknowledge: use GlobRef.t instead of Constr.t as entry
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 64c93a2607..62c14f6f07 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -693,12 +693,12 @@ let register_one env field entry = { env with retroknowledge = Retroknowledge.add_field env.retroknowledge field entry } (* [register env field entry] may register several fields when needed *) -let register env field entry = +let register env field gr = match field with - | 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 Int31Constructor) i31c) field entry - | field -> register_one env field entry + | KInt31 Int31Type -> + let i31c = match gr with + | GlobRef.IndRef i31t -> GlobRef.ConstructRef (i31t, 1) + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") + in + register_one (register_one env (KInt31 Int31Constructor) i31c) field gr + | field -> register_one env field gr |