diff options
Diffstat (limited to 'kernel/retypeops.ml')
| -rw-r--r-- | kernel/retypeops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml index dc1aa20310..61fabfee9f 100644 --- a/kernel/retypeops.ml +++ b/kernel/retypeops.ml @@ -30,7 +30,7 @@ let relevance_of_constant env c = let relevance_of_constructor env ((mi,i),_) = let decl = lookup_mind mi env in let packet = decl.mind_packets.(i) in - packet.mind_relevant + packet.mind_relevance let relevance_of_projection env p = let mind = Projection.mind p in |