aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/extraction.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/extraction.ml')
-rw-r--r--plugins/extraction/extraction.ml4
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. *)