diff options
| author | Pierre-Marie Pédrot | 2021-03-08 18:35:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-10 12:16:19 +0100 |
| commit | 8873ff0541e1902608d5d87b8158ff6b1d6f9d89 (patch) | |
| tree | ba058f3a73b5b252d02e9a26051e0a38fc4fb778 /kernel/nativecode.ml | |
| parent | e16a73156d92a6510e34e54a829f43f294820646 (diff) | |
Allow the presence of type casts for return values in Ltac2.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions