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.mli | |
| 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.mli')
| -rw-r--r-- | plugins/ltac/pptactic.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 79e0adf9f7..4f58eceb59 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -106,7 +106,7 @@ val pr_may_eval : val pr_and_short_name : ('a -> Pp.t) -> 'a Genredexpr.and_short_name -> Pp.t -val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t +val pr_evaluable_reference_env : env -> Tacred.evaluable_global_reference -> Pp.t val pr_quantified_hypothesis : quantified_hypothesis -> Pp.t |