diff options
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:= |