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 /printing/printmod.ml | |
| parent | 195772efccbac6663501bd5fff63c318d22ee191 (diff) | |
| parent | c51fb2fae0e196012de47203b8a71c61720d6c5c (diff) | |
Merge PR #10498: [api] Deprecate GlobRef constructors.
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 74d4f69c9c..43992ec9d3 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -15,7 +15,6 @@ open Pp open Names open Environ open Declarations -open Globnames open Libnames open Goptions @@ -231,13 +230,13 @@ let nametab_register_body mp dir (l,body) = | SFBmodule _ -> () (* TODO *) | SFBmodtype _ -> () (* TODO *) | SFBconst _ -> - push (Label.to_id l) (ConstRef (Constant.make2 mp l)) + push (Label.to_id l) (GlobRef.ConstRef (Constant.make2 mp l)) | SFBmind mib -> let mind = MutInd.make2 mp l in Array.iteri (fun i mip -> - push mip.mind_typename (IndRef (mind,i)); - Array.iteri (fun j id -> push id (ConstructRef ((mind,i),j+1))) + push mip.mind_typename (GlobRef.IndRef (mind,i)); + Array.iteri (fun j id -> push id (GlobRef.ConstructRef ((mind,i),j+1))) mip.mind_consnames) mib.mind_packets |