diff options
| author | Gaëtan Gilbert | 2019-07-11 12:18:18 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-11 12:18:18 +0200 |
| commit | b424691372a61de64b8b9a8c94ef0c9cb61c7274 (patch) | |
| tree | 60c2cc24ad7550f07cb06aedfb2a3c5402f016ce /plugins/firstorder/ground.ml | |
| parent | 195772efccbac6663501bd5fff63c318d22ee191 (diff) | |
| parent | c51fb2fae0e196012de47203b8a71c61720d6c5c (diff) | |
Merge PR #10498: [api] Deprecate GlobRef constructors.
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Diffstat (limited to 'plugins/firstorder/ground.ml')
| -rw-r--r-- | plugins/firstorder/ground.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index bdf339a488..e134562702 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -15,12 +15,11 @@ open Rules open Instances open Tacmach.New open Tacticals.New -open Globnames let update_flags ()= let open TransparentState in let f accu coe = match coe.Classops.coe_value with - | ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst } + | Names.GlobRef.ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst } | _ -> accu in let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in |