aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/extract_env.ml2
-rw-r--r--plugins/extraction/extraction.ml8
2 files changed, 5 insertions, 5 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 39826d744..89c2a0ae3 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -132,7 +132,7 @@ let rec add_labels mp = function
exception Impossible
let check_arity env cb =
- let t = Typeops.type_of_constant_type env cb.const_type in
+ let t = cb.const_type in
if Reduction.is_arity env t then raise Impossible
let check_fix env cb i =
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 3661faada..661842790 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -518,7 +518,7 @@ and mlt_env env r = match r with
match lookup_typedef kn cb with
| Some _ as o -> o
| None ->
- let typ = Typeops.type_of_constant_type env cb.const_type
+ let typ = cb.const_type
(* FIXME not sure if we should instantiate univs here *) in
match flag_of_type env typ with
| Info,TypeScheme ->
@@ -543,7 +543,7 @@ let record_constant_type env kn opt_typ =
| Some schema -> schema
| None ->
let typ = match opt_typ with
- | None -> Typeops.type_of_constant_type env cb.const_type
+ | None -> cb.const_type
| Some typ -> typ
in
let mlt = extract_type env [] 1 typ [] in
@@ -969,7 +969,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
let extract_constant env kn cb =
let r = ConstRef kn in
- let typ = Typeops.type_of_constant_type env cb.const_type in
+ let typ = cb.const_type in
let warn_info () = if not (is_custom r) then add_info_axiom r in
let warn_log () = if not (constant_has_body cb) then add_log_axiom r
in
@@ -1025,7 +1025,7 @@ let extract_constant env kn cb =
let extract_constant_spec env kn cb =
let r = ConstRef kn in
- let typ = Typeops.type_of_constant_type env cb.const_type in
+ let typ = cb.const_type in
try
match flag_of_type env typ with
| (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))