From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- kernel/declareops.ml | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) (limited to 'kernel/declareops.ml') diff --git a/kernel/declareops.ml b/kernel/declareops.ml index a7051d5c..248504c1 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -304,17 +304,7 @@ let hcons_mind mib = (** {6 Stm machinery } *) -let string_of_side_effect = function - | SEsubproof (c,_,_) -> Names.string_of_con c - | SEscheme (cl,_) -> - String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) -type side_effects = side_effect list -let no_seff = ([] : side_effects) -let iter_side_effects f l = List.iter f (List.rev l) -let fold_side_effects f a l = List.fold_left f a l -let uniquize_side_effects l = List.rev (CList.uniquize (List.rev l)) -let union_side_effects l1 l2 = l1 @ l2 -let flatten_side_effects l = List.flatten l -let side_effects_of_list l = l -let cons_side_effects x l = x :: l -let side_effects_is_empty = List.is_empty +let string_of_side_effect { Entries.eff } = match eff with + | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")" + | Entries.SEscheme (cl,_) -> + "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")" -- cgit v1.2.3