aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarconv.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2019-12-24 16:52:06 +0100
committerThéo Zimmermann2019-12-24 16:52:06 +0100
commitfeea1d0377e2fb083efe74cd241e7867d008d5be (patch)
tree2a6b9d45182d2d9eb1af3f9f3dbaa288111f0528 /pretyping/evarconv.ml
parent23eb6e3805738ad244f37e73c34e0488dc9c71f8 (diff)
parent8ca6ef52ae0091a694b1047ca1ca53d7d836a3a3 (diff)
Merge PR #11284: [meta] Add ltac2 information to META.
Ack-by: Zimmi48
Diffstat (limited to 'pretyping/evarconv.ml')
0 files changed, 0 insertions, 0 deletions