Merge PR #889: Removing template polymorphism for definitions.

1 files changed, 5 insertions, 9 deletions

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