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/tacintern.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/tacintern.ml')
| -rw-r--r-- | plugins/ltac/tacintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 8bee7afa2c..ae7a10ce52 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -308,8 +308,8 @@ let short_name qid = else None let evalref_of_globref ?loc ?short = function - | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short) - | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short) + | GlobRef.ConstRef cst -> ArgArg (Tacred.EvalConstRef cst, short) + | GlobRef.VarRef id -> ArgArg (Tacred.EvalVarRef id, short) | r -> let tpe = match r with | GlobRef.IndRef _ -> "inductive" |