aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses_errors.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-06-24 21:44:08 +0200
committerPierre-Marie Pédrot2020-07-05 21:41:08 +0200
commita659a12ca88bebaf1fa7f201023cc06be34849d9 (patch)
tree2fd34dc2ca30a7f0bfda0d53a788d6785e073e1d /pretyping/typeclasses_errors.ml
parent5c1730ca2533b17066e7ee5c672ae6aa5fdef1dc (diff)
Inline the Reductionops.fix_recarg function.
It was only used in Tacred, and with a type that forced to perform a change of representation of stacks.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions