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/ltac/pptactic.ml | |
| parent | 195772efccbac6663501bd5fff63c318d22ee191 (diff) | |
| parent | c51fb2fae0e196012de47203b8a71c61720d6c5c (diff) | |
Merge PR #10498: [api] Deprecate GlobRef constructors.
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index db8d09b79e..0e38ce575b 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -194,7 +194,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_evaluable_reference = function | EvalVarRef id -> pr_id id - | EvalConstRef sp -> pr_global (Globnames.ConstRef sp) + | EvalConstRef sp -> pr_global (GlobRef.ConstRef sp) let pr_quantified_hypothesis = function | AnonHyp n -> int n @@ -385,7 +385,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_evaluable_reference_env env = function | EvalVarRef id -> pr_id id | EvalConstRef sp -> - Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp) + Nametab.pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef sp) let pr_as_disjunctive_ipat prc ipatl = keyword "as" ++ spc () ++ |