diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 979240663..455965af4 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -34,9 +34,17 @@ let current_fixpoints = ref ([] : constant list) let none = Evd.empty -let type_of env c = Retyping.get_type_of env none (strip_outer_cast c) +let type_of env c = + try + let polyprop = (lang() = Haskell) in + Retyping.get_type_of ~polyprop env none (strip_outer_cast c) + with SingletonInductiveBecomesProp id -> error_singleton_become_prop id -let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c) +let sort_of env c = + try + let polyprop = (lang() = Haskell) in + Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c) + with SingletonInductiveBecomesProp id -> error_singleton_become_prop id (*S Generation of flags and signatures. *) |