diff options
| author | Maxime Dénès | 2018-07-20 18:01:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-07-26 14:42:45 +0200 |
| commit | f54192a50eaf14852e1462f24e4168aa8a8545fe (patch) | |
| tree | 64696d9c111f420e9bff7d7f742602a6b38f8b0a /plugins/firstorder | |
| parent | 85d5f45d7a5374646a31f8829965bbfed0a95070 (diff) | |
Coercions cleanup: use GlobRef.t instead of constr
Diffstat (limited to 'plugins/firstorder')
| -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 4e3ba57308..3901a951f0 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -13,17 +13,16 @@ 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 coe = + match coe.Classops.coe_value with + | ConstRef c -> predref := Names.Cpred.add c !predref + | _ -> () in List.iter f (Classops.coercions ()); red_flags:= |