diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-13 12:49:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-13 12:49:54 +0200 |
| commit | f3b84cf63c242623bdcccd30c536e55983971da5 (patch) | |
| tree | 740984c577ed75c76edc2525b3de9bf744da3c21 /parsing/egramcoq.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 'parsing/egramcoq.ml')
0 files changed, 0 insertions, 0 deletions