diff options
Diffstat (limited to 'export/ExportBase.ml')
| -rw-r--r-- | export/ExportBase.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/export/ExportBase.ml b/export/ExportBase.ml index 4b93d8a9..b6388768 100644 --- a/export/ExportBase.ml +++ b/export/ExportBase.ml @@ -219,6 +219,7 @@ let external_function p = function coqstring text signatur sg (print_list coqstring) clob + | EF_profiling(_ ,_) -> failwith "EF_profiling in export" (* Variables *) |