diff options
| author | Maxime Dénès | 2018-07-26 14:40:06 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-07-26 14:42:45 +0200 |
| commit | baf8b6e100c49635c56308f17275b963d4f5253c (patch) | |
| tree | f92fb7cbc84396ce3fb132db65e70f7a24735568 /plugins | |
| parent | dfacbac8dada1bfe9bcb55fcbd97375fe06e245c (diff) | |
Replace iter + ref by fold_left
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/firstorder/ground.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 3901a951f0..516b04ea21 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -18,17 +18,16 @@ open Tacticals.New open Globnames let update_flags ()= - let predref=ref Names.Cpred.empty in - let f coe = + let f acc coe = match coe.Classops.coe_value with - | ConstRef c -> predref := Names.Cpred.add c !predref - | _ -> () + | ConstRef c -> Names.Cpred.add c acc + | _ -> acc in - List.iter f (Classops.coercions ()); + let pred = List.fold_left f Names.Cpred.empty (Classops.coercions ()) in red_flags:= CClosure.RedFlags.red_add_transparent CClosure.betaiotazeta - (Names.Id.Pred.full,Names.Cpred.complement !predref) + (Names.Id.Pred.full,Names.Cpred.complement pred) let ground_tac solver startseq = Proofview.Goal.enter begin fun gl -> |