diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 22:50:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 15:59:10 +0200 |
| commit | c51fb2fae0e196012de47203b8a71c61720d6c5c (patch) | |
| tree | e49c2d38b6c841dc6514944750d21ed08ab94bce /plugins/omega | |
| parent | 437063a0c745094c5693d1c5abba46ce375d69c6 (diff) | |
[api] Deprecate GlobRef constructors.
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
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 6aec83318c..3b79a130f2 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") |