diff options
| -rw-r--r-- | contrib/extraction/extraction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 37b8b4492e..cfd4e33faa 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -263,7 +263,7 @@ let prop_abstract f = (*s Abstraction of an constant. *) let abstract_constant sp s = - if s = [] then MLglob (ConstRef sp) + if List.for_all ((=) default) s then MLglob (ConstRef sp) else let f a = if List.mem default s then MLapp (MLglob (ConstRef sp), a) |