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/omega | |
| parent | 195772efccbac6663501bd5fff63c318d22ee191 (diff) | |
| parent | c51fb2fae0e196012de47203b8a71c61720d6c5c (diff) | |
Merge PR #10498: [api] Deprecate GlobRef constructors.
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 776bd0a829..00ea9b6a66 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -27,7 +27,6 @@ open Tacmach.New open Tactics open Logic open Libnames -open Globnames open Nametab open Contradiction open Tactypes @@ -426,11 +425,11 @@ let destructurate_prop sigma t = | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args) | _, [_;_] when eq_constr c (Lazy.force coq_gt) -> Kapp (Gt,args) | Const (sp,_), args -> - Kapp (Other (string_of_path (path_of_global (ConstRef sp))),args) + Kapp (Other (string_of_path (path_of_global (GlobRef.ConstRef sp))),args) | Construct (csp,_) , args -> - Kapp (Other (string_of_path (path_of_global (ConstructRef csp))), args) + Kapp (Other (string_of_path (path_of_global (GlobRef.ConstructRef csp))), args) | Ind (isp,_), args -> - Kapp (Other (string_of_path (path_of_global (IndRef isp))),args) + Kapp (Other (string_of_path (path_of_global (GlobRef.IndRef isp))),args) | Var id,[] -> Kvar id | Prod ({binder_name=Anonymous},typ,body), [] -> Kimp(typ,body) | Prod ({binder_name=Name _},_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal") |