diff options
| author | Pierre-Marie Pédrot | 2020-10-29 13:59:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-21 13:55:32 +0100 |
| commit | 63332cbd4ac59b39fdce63d9872aa52dd8a2fec6 (patch) | |
| tree | 9913737179ee72e0c1b9672227fe5872ce6734a9 /plugins/ltac/pptactic.ml | |
| parent | a714abe0a1c0cac277297f9e3c7f6d90ac0173d6 (diff) | |
Move evaluable_global_reference from Names to Tacred.
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index faad792ea9..6ebb01703f 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -191,8 +191,8 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_and_short_name pr (c,_) = pr c let pr_evaluable_reference = function - | EvalVarRef id -> pr_id id - | EvalConstRef sp -> pr_global (GlobRef.ConstRef sp) + | Tacred.EvalVarRef id -> pr_id id + | Tacred.EvalConstRef sp -> pr_global (GlobRef.ConstRef sp) let pr_quantified_hypothesis = function | AnonHyp n -> int n @@ -381,8 +381,8 @@ let string_of_genarg_arg (ArgumentType arg) = str "<" ++ KerName.print kn ++ str ">" let pr_evaluable_reference_env env = function - | EvalVarRef id -> pr_id id - | EvalConstRef sp -> + | Tacred.EvalVarRef id -> pr_id id + | Tacred.EvalConstRef sp -> Nametab.pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef sp) let pr_as_disjunctive_ipat prc ipatl = |