aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-17 12:57:43 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-26 15:17:12 +0200
commitd9530632321c0b470ece6337cda2cf54d02d61eb (patch)
treedd8ef37eddb9a3244c85e7cf042c5168edc95e12 /plugins
parent906b48ff401f22be6059a6cdde8723b858102690 (diff)
Removing template polymorphism for definitions.
The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless.
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/extract_env.ml2
-rw-r--r--plugins/extraction/extraction.ml8
-rw-r--r--plugins/funind/indfun.ml2
3 files changed, 6 insertions, 6 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))
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 863c9dc8d..89537ad3f 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -857,7 +857,7 @@ let make_graph (f_ref:global_reference) =
with_full_print (fun () ->
(Constrextern.extern_constr false env sigma body,
Constrextern.extern_type false env sigma
- ((*FIXME*) Typeops.type_of_constant_type env c_body.const_type)
+ ((*FIXME*) c_body.const_type)
)
)
()