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.
---
 checker/mod_checking.ml | 14 +++++---------
 1 file changed, 5 insertions(+), 9 deletions(-)

(limited to 'checker/mod_checking.ml')

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 4948f6008f..b6816dd484 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -35,15 +35,11 @@ let check_constant_declaration env kn cb =
       push_context ~strict:false ctx env
   in
   let envty, ty = 
-    match cb.const_type with
-      RegularArity ty ->
-        let ty', cu = refresh_arity ty in
-        let envty = push_context_set cu env' in
-        let _ = infer_type envty ty' in envty, ty
-    | TemplateArity(ctxt,par) ->
-        let _ = check_ctxt env' ctxt in
-        check_polymorphic_arity env' ctxt par;
-	env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt 
+    let ty = cb.const_type in
+    let ty', cu = refresh_arity ty in
+    let envty = push_context_set cu env' in
+    let _ = infer_type envty ty' in
+    envty, ty
   in
   let () = 
     match body_of_constant cb with
-- 
cgit v1.2.3