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 /pretyping/typeclasses.ml | |
| parent | 195772efccbac6663501bd5fff63c318d22ee191 (diff) | |
| parent | c51fb2fae0e196012de47203b8a71c61720d6c5c (diff) | |
Merge PR #10498: [api] Deprecate GlobRef constructors.
Reviewed-by: SkySkimmer
Ack-by: ppedrot
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 |