From d9530632321c0b470ece6337cda2cf54d02d61eb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 17 Jul 2017 12:57:43 +0200
Subject: 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.
---
 pretyping/evarsolve.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 9f48297613..ef0fb8ea6e 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -34,12 +34,6 @@ let get_polymorphic_positions sigma f =
       (match oib.mind_arity with
       | RegularArity _ -> assert false
       | TemplateArity templ -> templ.template_param_levels)
-  | Const (cst, u) ->
-    let cb = Global.lookup_constant cst in
-      (match cb.const_type with
-      | RegularArity _ -> assert false
-      | TemplateArity (_, templ) -> 
-        templ.template_param_levels)
   | _ -> assert false
 
 let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
-- 
cgit v1.2.3