diff options
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index e13fb4f08..cf0f715be 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -292,11 +292,6 @@ let hcons_mind mib = (** {6 Stm machinery } *) -let join_constant_body otab cb = - match cb.const_body with - | OpaqueDef o -> Opaqueproof.join_opaque otab o - | _ -> () - let string_of_side_effect = function | SEsubproof (c,_,_) -> Names.string_of_con c | SEscheme (cl,_) -> |