diff options
author | 2018-04-13 12:49:54 +0200 | |
---|---|---|
committer | 2018-04-13 12:49:54 +0200 | |
commit | f3b84cf63c242623bdcccd30c536e55983971da5 (patch) | |
tree | 740984c577ed75c76edc2525b3de9bf744da3c21 /pretyping/cbv.ml | |
parent | b68e0b4f9ba37d1c2fa5921e1d934b4b38bfdfe7 (diff) | |
parent | 9f723f14e5342c1303646b5ea7bb5c0012a090ef (diff) |
Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contains evars
Diffstat (limited to 'pretyping/cbv.ml')
0 files changed, 0 insertions, 0 deletions