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 /pretyping/typeclasses.ml | |
| 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 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 1d3e77452f..544fd3d17d 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -205,7 +205,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = | Some p, None -> Some (p + 1) | _, _ -> None in - Some (ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs + Some (GlobRef.ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs in let declare_proj hints (cref, info, body) = let path' = cref :: path in @@ -243,11 +243,11 @@ let instance_constructor (cl,u) args = let open EConstr in let pars = fst (List.chop lenpars args) in match cl.cl_impl with - | IndRef ind -> + | GlobRef.IndRef ind -> let ind = ind, u in (Some (applist (mkConstructUi (ind, 1), args)), applist (mkIndU ind, pars)) - | ConstRef cst -> + | GlobRef.ConstRef cst -> let cst = cst, u in let term = match args with | [] -> None |