diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 23:34:07 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-25 13:37:03 +0100 |
commit | c4d62e3686926c27b172636ca8b746814d13a462 (patch) | |
tree | c7a627b0fb392e187fe0cd72ed39656d56b81504 /pretyping/miscops.ml | |
parent | a54579dd20e04ea919f8fa887e15dd82051fa297 (diff) |
Moving type_uconstr to Pretyping.
Diffstat (limited to 'pretyping/miscops.ml')
0 files changed, 0 insertions, 0 deletions