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 /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/tacmach.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 08f88d46c1..6a6dd783e4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -69,7 +69,7 @@ val pf_reduce_to_atomic_ind : Goal.goal sigma -> types -> (inductive * EInst [@@ocaml.deprecated "Use Tacred.pf_reduce_to_atomic_ind"] val pf_compute : Goal.goal sigma -> constr -> constr [@@ocaml.deprecated "Use the version in Tacmach.New"] -val pf_unfoldn : (occurrences * evaluable_global_reference) list +val pf_unfoldn : (occurrences * Tacred.evaluable_global_reference) list -> Goal.goal sigma -> constr -> constr [@@ocaml.deprecated "Use Tacred.unfoldn"] |