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/modops.ml | |
| parent | 42bed627c4a1c5a1ecf59d4865fc872b5eee7290 (diff) | |
Retroknowledge: use GlobRef.t instead of Constr.t as entry
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 98a9973117..9435f46c6b 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -267,7 +267,7 @@ let subst_structure subst = subst_structure subst do_delta_codom (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) let add_retroknowledge = let perform rkaction env = match rkaction with - | Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> + | Retroknowledge.RKRegister (f, ((GlobRef.ConstRef _ | GlobRef.IndRef _) as e)) -> Environ.register env f e | _ -> CErrors.anomaly ~label:"Modops.add_retroknowledge" |