diff options
| author | Enrico Tassi | 2018-07-27 08:55:30 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-07-27 08:55:30 +0200 |
| commit | e7c1b08bbb300d31e82ca6c457fd4e3050239b9d (patch) | |
| tree | 6813ef46499b6de0d532d97946374e274e587b58 /plugins/firstorder | |
| parent | 9f9a7736c24270a3f3d8177c65e80a1ee04c4615 (diff) | |
| parent | baf8b6e100c49635c56308f17275b963d4f5253c (diff) | |
Merge PR #8103: Coercions cleanup: use GlobRef.t instead of constr
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/ground.ml | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 4e3ba57308..516b04ea21 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -13,23 +13,21 @@ open Formula open Sequent open Rules open Instances -open Constr open Tacmach.New open Tacticals.New +open Globnames let update_flags ()= - let predref=ref Names.Cpred.empty in - let f coe= - try - let kn= fst (destConst (Classops.get_coercion_value coe)) in - predref:=Names.Cpred.add kn !predref - with DestKO -> () + let f acc coe = + match coe.Classops.coe_value with + | 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 -> |