From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 20:09:26 +0100 Subject: Eliminating parts of the right-hand side compatibility layer --- plugins/extraction/extraction.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/extraction') 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. *) -- cgit v1.2.3