aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-11-28 16:18:46 +0100
committerGaëtan Gilbert2018-11-28 16:18:46 +0100
commit58e5071189bf60aadb35aaafb7016615557be7de (patch)
tree7b0d5daac68596c30158e3848e7566d90c1d3bda /pretyping/typeclasses.ml
parent2e36fbcac4a04d4f29925ba09f441db6426b7af1 (diff)
parentabdc6b34b11ac1ccbcb8c48291b74c6762fc7573 (diff)
Merge PR #7153: Make OrderedTypeFullFacts a module functor
Diffstat (limited to 'pretyping/typeclasses.ml')
0 files changed, 0 insertions, 0 deletions