diff options
| author | Maxime Dénès | 2018-09-03 12:41:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-03 12:41:46 +0200 |
| commit | da58ae4c620412923ea84b1982e8765f6be145a8 (patch) | |
| tree | 8518269959c007a7c70bdbd80a968ebff03c6415 /kernel/declareops.ml | |
| parent | 3bc0c82700a805e889198b810cc0148f6479cbe1 (diff) | |
| parent | 568f3b69d407f7b5a47d1fdd6ca2bbf3edb5be72 (diff) | |
Merge PR #7912: Simplify effects API
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index b0d8410873..51ec3defb3 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -306,13 +306,6 @@ let hcons_mind mib = mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; mind_universes = hcons_mind_universes mib.mind_universes } -(** {6 Stm machinery } *) - -let string_of_side_effect { Entries.eff } = match eff with - | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.Constant.to_string c ^ ")" - | Entries.SEscheme (cl,_) -> - "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.Constant.to_string c) cl) ^ ")" - (** Hashconsing of modules *) let hcons_functorize hty he hself f = match f with |