Fix checking of constants in checker. Prelude can now be checked.

1 files changed, 19 insertions, 14 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 12a97bf68..93b136c48 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -25,22 +25,27 @@ let refresh_arity ar =
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn);
-  let env = add_constraints (Univ.UContext.constraints cb.const_universes) env in
-  (match cb.const_type with
+  let env' = add_constraints (Univ.UContext.constraints cb.const_universes) env in
+  let envty, ty = 
+    match cb.const_type with
       RegularArity ty ->
-        let ty, cu = refresh_arity ty in
-        let envty = add_constraints cu env in
-        let _ = infer_type envty ty in
-        (match body_of_constant cb with
-          | Some bd ->
-              let j = infer envty bd in
-              conv_leq envty j ty
-          | None -> ())
+        let ty', cu = refresh_arity ty in
+        let envty = add_constraints 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);
-  add_constant kn cb env
-
+        let _ = check_ctxt env' ctxt in
+        check_polymorphic_arity env' ctxt par;
+	env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt 
+  in
+  let body = 
+    match body_of_constant cb with
+    | Some bd ->
+      let j = infer envty bd in
+        conv_leq envty j ty
+    | None -> ()
+  in
+  if cb.const_polymorphic then add_constant kn cb env
+  else add_constant kn cb env'
 
 (** {6 Checking modules } *)