diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
-rw-r--r-- | plugins/extraction/extraction.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index e9fd40722..460157130 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -42,11 +42,11 @@ let none = Evd.empty let type_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_type_of ~polyprop env none (EConstr.of_constr (strip_outer_cast none (EConstr.of_constr c))) + Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) let sort_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_sort_family_of ~polyprop env none (EConstr.of_constr (strip_outer_cast none (EConstr.of_constr c))) + Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) (*S Generation of flags and signatures. *) |