Repair relevance marks in-kernel.

Prevent errors when under annotating binders.

11 files changed, 169 insertions, 129 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 14cfba187e..5551742c02 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -177,7 +177,7 @@ type one_inductive_body = {
 
     mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
 
-    mind_relevant : Sorts.relevance;
+    mind_relevance : Sorts.relevance;
 
 (** {8 Datas for bytecode compilation } *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index da5217eb33..de9a052096 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -223,7 +223,7 @@ let subst_mind_packet sub mbp =
     mind_nrealdecls = mbp.mind_nrealdecls;
     mind_kelim = mbp.mind_kelim;
     mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
-    mind_relevant = mbp.mind_relevant;
+    mind_relevance = mbp.mind_relevance;
     mind_nb_constant = mbp.mind_nb_constant;
     mind_nb_args = mbp.mind_nb_args;
     mind_reloc_tbl = mbp.mind_reloc_tbl }
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index ff2c91d913..4e6e595331 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -303,8 +303,7 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
   in
 
   (* Params *)
-  let env_params = Typeops.check_context env_univs mie.mind_entry_params in
-  let params = Environ.rel_context env_params in
+  let env_params, params = Typeops.check_context env_univs mie.mind_entry_params in
 
   (* Arities *)
   let env_ar, data = List.fold_left_map (check_arity env_params) env_univs mie.mind_entry_inds in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 3173dc5383..009eb3da38 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -173,7 +173,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) =
   let specif = (lookup_mind_specif env mi, u) in
   let ty = type_of_inductive env specif in
   let env' =
-    let r = (snd (fst specif)).mind_relevant in
+    let r = (snd (fst specif)).mind_relevance in
     let anon = Context.make_annot Anonymous r in
     let decl = LocalAssum (anon, hnf_prod_applist env ty lrecparams) in
     push_rel decl env in
@@ -486,7 +486,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
     let consnrealargs =
       Array.map (fun (d,_) -> Context.Rel.nhyps d)
         splayed_lc in
-    let mind_relevant = match arity with
+    let mind_relevance = match arity with
       | RegularArity { mind_sort;_ } -> Sorts.relevance_of_sort mind_sort
       | TemplateArity _ -> Sorts.Relevant
     in
@@ -517,7 +517,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
 	mind_user_lc = lc;
 	mind_nf_lc = nf_lc;
         mind_recargs = recarg;
-        mind_relevant;
+        mind_relevance;
         mind_nb_constant = !nconst;
 	mind_nb_args = !nblock;
 	mind_reloc_tbl = rtbl;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2d34c02302..7452038ba5 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -196,7 +196,7 @@ let instantiate_universes env ctx ar argsorts =
 
 let relevance_of_inductive env ind =
   let _, mip = lookup_mind_specif env ind in
-  mip.mind_relevant
+  mip.mind_relevance
 
 let type_of_inductive_gen ?(polyprop=true) env ((_,mip),u) paramtyps =
   match mip.mind_arity with
@@ -579,7 +579,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
   let mib = Environ.lookup_mind mind env in
   let ntypes = mib.mind_ntypes in
   let push_ind specif env =
-    let r = specif.mind_relevant in
+    let r = specif.mind_relevance in
     let anon = Context.make_annot Anonymous r in
     let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in
     push_rel decl env
@@ -1080,7 +1080,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
     let ((ind, _), _) as res = check_occur fixenv 1 def in
     let _, ind = lookup_mind_specif env ind in
     (* recursive sprop means non record with projections -> squashed *)
-    if Sorts.Irrelevant == ind.mind_relevant
+    if Sorts.Irrelevant == ind.mind_relevance
     then
       begin
         if names.(i).Context.binder_relevance == Sorts.Relevant
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 421d932d9a..2de5faa6df 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -80,6 +80,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
           let c',cst = match cb.const_body with
             | Undef _ | OpaqueDef _ ->
               let j = Typeops.infer env' c in
+              assert (j.uj_val == c); (* relevances should already be correct here *)
               let typ = cb.const_type in
               let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
                   j.uj_type typ in
@@ -101,6 +102,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
           let cst = match cb.const_body with
             | Undef _ | OpaqueDef _ ->
               let j = Typeops.infer env' c in
+              assert (j.uj_val == c); (* relevances should already be correct here *)
               let typ = cb.const_type in
               let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
                   j.uj_type typ in
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index b1d177e76d..2dab14e732 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1946,7 +1946,7 @@ let compile_mind mb mind stack =
       let tbl = ob.mind_reloc_tbl in
       (* Building info *)
       let ci = { ci_ind = ind; ci_npar = nparams;
-                 ci_cstr_nargs = [|0|]; ci_relevance = ob.mind_relevant;
+                 ci_cstr_nargs = [|0|]; ci_relevance = ob.mind_relevance;
                  ci_cstr_ndecls = [||] (*FIXME*);
                  ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in
       let asw = { asw_ind = ind; asw_prefix = ""; asw_ci = ci;
diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml
index dc1aa20310..61fabfee9f 100644
--- a/kernel/retypeops.ml
+++ b/kernel/retypeops.ml
@@ -30,7 +30,7 @@ let relevance_of_constant env c =
 let relevance_of_constructor env ((mi,i),_) =
   let decl = lookup_mind mi env in
   let packet = decl.mind_packets.(i) in
-  packet.mind_relevant
+  packet.mind_relevance
 
 let relevance_of_projection env p =
   let mind = Projection.mind p in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index af96cfdb4f..f773f800c6 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -21,7 +21,6 @@ open Constr
 open Declarations
 open Environ
 open Entries
-open Typeops
 
 module NamedDecl = Context.Named.Declaration
 
@@ -72,10 +71,10 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         | Monomorphic_entry uctx -> push_context_set ~strict:true uctx env
         | Polymorphic_entry (_, uctx) -> push_context ~strict:false uctx env
       in
-      let j = infer env t in
+      let j = Typeops.infer env t in
       let usubst, univs = Declareops.abstract_universes uctx in
-      let c, r = Typeops.assumption_of_judgment env j in
-      let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in
+      let r = Typeops.assumption_of_judgment env j in
+      let t = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in
       {
         Cooking.cook_body = Undef nl;
         cook_type = t;
@@ -94,12 +93,12 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       let env = push_context_set ~strict:true uctxt env in
       let ty = match otyp with
       | Some typ ->
-        let tyj = infer_type env typ in
-        check_primitive_type env op_t tyj.utj_val;
-        Constr.hcons tyj.utj_val
+        let typ = Typeops.infer_type env typ in
+        Typeops.check_primitive_type env op_t typ.utj_val;
+        Constr.hcons typ.utj_val
       | None ->
         match op_t with
-        | CPrimitives.OT_op op -> type_of_prim env op
+        | CPrimitives.OT_op op -> Typeops.type_of_prim env op
         | CPrimitives.OT_type _ -> mkSet
       in
       let cd =
@@ -130,8 +129,8 @@ the polymorphic case
                        const_entry_opaque = true;
                        const_entry_universes = Monomorphic_entry univs; _ } as c) ->
       let env = push_context_set ~strict:true univs env in
-      let { const_entry_body = body; const_entry_feedback = feedback_id ; _ } = c in
-      let tyj = infer_type env typ in
+      let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
+      let tyj = Typeops.infer_type env typ in
       let proofterm =
         Future.chain body (fun ((body,uctx),side_eff) ->
           (* don't redeclare universes which are declared for the type *)
@@ -139,17 +138,17 @@ the polymorphic case
           let j, uctx = match trust with
           | Pure ->
             let env = push_context_set uctx env in
-            let j = infer env body in
-            let _ = judge_of_cast env j DEFAULTcast tyj in
+            let j = Typeops.infer env body in
+            let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in
             j, uctx
           | SideEffects handle ->
             let (body, uctx', valid_signatures) = handle env body side_eff in
             let uctx = Univ.ContextSet.union uctx uctx' in
             let env = push_context_set uctx env in
             let body,env,ectx = skip_trusted_seff valid_signatures body env in
-            let j = infer env body in
+            let j = Typeops.infer env body in
             let j = unzip ectx j in
-            let _ = judge_of_cast env j DEFAULTcast tyj in
+            let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in
             j, uctx
           in
           let c = Constr.hcons j.uj_val in
@@ -158,7 +157,7 @@ the polymorphic case
       let def = OpaqueDef (Opaqueproof.create proofterm) in
       {
         Cooking.cook_body = def;
-        cook_type = typ;
+        cook_type = tyj.utj_val;
         cook_universes = Monomorphic univs;
         cook_private_univs = None;
         cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
@@ -197,14 +196,14 @@ the polymorphic case
         in
         env, sbst, Polymorphic auctx, local
       in
-      let j = infer env body in
+      let j = Typeops.infer env body in
       let typ = match typ with
         | None ->
           Vars.subst_univs_level_constr usubst j.uj_type
         | Some t ->
-           let tj = infer_type env t in
-           let _ = judge_of_cast env j DEFAULTcast tj in
-           Vars.subst_univs_level_constr usubst t
+           let tj = Typeops.infer_type env t in
+           let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
+           Vars.subst_univs_level_constr usubst tj.utj_val
       in
       let def = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
@@ -217,7 +216,7 @@ the polymorphic case
         cook_type = typ;
         cook_universes = univs;
         cook_private_univs = private_univs;
-        cook_relevance = Retypeops.relevance_of_term env body;
+        cook_relevance = Retypeops.relevance_of_term env j.uj_val;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
       }
@@ -324,9 +323,9 @@ let translate_constant mb env kn ce =
     (infer_declaration ~trust:mb env ce)
 
 let translate_local_assum env t =
-  let j = infer env t in
+  let j = Typeops.infer env t in
   let t = Typeops.assumption_of_judgment env j in
-    t
+    j.uj_val, t
 
 let translate_recipe ~hcons env kn r =
   build_constant_declaration kn env (Cooking.cook_constant ~hcons r)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 337b66e8e7..be878dd99b 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -15,6 +15,7 @@ open Univ
 open Sorts
 open Term
 open Constr
+open Context
 open Vars
 open Declarations
 open Environ
@@ -51,15 +52,28 @@ let check_type env c t =
 let infer_assumption env t ty =
   try
     let s = check_type env t ty in
-    t, (match s with Sorts.SProp -> Irrelevant | _ -> Relevant)
+    (match s with Sorts.SProp -> Irrelevant | _ -> Relevant)
   with TypeError _ ->
     error_assumption env (make_judge t ty)
 
+let warn_bad_relevance_name = "bad-relevance"
+let warn_bad_relevance =
+  CWarnings.create ~name:warn_bad_relevance_name ~category:"debug" ~default:CWarnings.Disabled
+    Pp.(function
+        | None ->  str "Bad relevance in case annotation."
+        | Some x -> str "Bad relevance for binder " ++ Name.print x.binder_name ++ str ".")
+
+let warn_bad_relevance_ci ?loc () = warn_bad_relevance ?loc None
+let warn_bad_relevance ?loc x = warn_bad_relevance ?loc (Some x)
+
 let check_assumption env x t ty =
-  let r = x.Context.binder_relevance in
-  let t, r' = infer_assumption env t ty in
-  if not (r == r') then error_bad_relevance env;
-  t
+  let r = x.binder_relevance in
+  let r' = infer_assumption env t ty in
+  let x = if Sorts.relevance_equal r r'
+    then x
+    else (warn_bad_relevance x; {x with binder_relevance = r'})
+  in
+  x
 
 (************************************************)
 (* Incremental typing rules: builds a typing judgment given the *)
@@ -388,11 +402,15 @@ let type_of_case env ci p pt c ct _lf lft =
     with Not_found -> error_case_not_inductive env (make_judge c ct) in
   let _, sp = try dest_arity env pt
     with NotArity -> error_elim_arity env pind c (make_judge p pt) None in
-  let () = check_case_info env pind (Sorts.relevance_of_sort sp) ci in
+  let rp = Sorts.relevance_of_sort sp in
+  let ci = if ci.ci_relevance == rp then ci
+    else (warn_bad_relevance_ci (); {ci with ci_relevance=rp})
+  in
+  let () = check_case_info env pind rp ci in
   let (bty,rslty) =
     type_case_branches env indspec (make_judge p pt) c in
   let () = check_branch_types env pind c ct lft bty in
-  rslty
+  ci, rslty
 
 let type_of_projection env p c ct =
   let pty = lookup_projection p env in
@@ -467,9 +485,12 @@ let constr_of_global_in_context env r =
 (************************************************************************)
 (************************************************************************)
 
-let check_binder_annot env s x =
-  let r = x.Context.binder_relevance in
-  if not (Sorts.relevance_of_sort s == r) then error_bad_relevance env
+let check_binder_annot s x =
+  let r = x.binder_relevance in
+  let r' = Sorts.relevance_of_sort s in
+  if r' == r
+  then x
+  else (warn_bad_relevance x; {x with binder_relevance = r'})
 
 (* The typing machine. *)
     (* ATTENTION : faudra faire le typage du contexte des Const,
@@ -483,91 +504,106 @@ let rec execute env cstr =
       (match s with
        | SProp -> if not (Environ.sprop_allowed env) then error_disallowed_sprop env
        | _ -> ());
-      type_of_sort s
+      cstr, type_of_sort s
 
     | Rel n ->
-      type_of_relative env n
+      cstr, type_of_relative env n
 
     | Var id ->
-      type_of_variable env id
+      cstr, type_of_variable env id
 
     | Const c ->
-      type_of_constant env c
+      cstr, type_of_constant env c
 	
     | Proj (p, c) ->
-        let ct = execute env c in
-          type_of_projection env p c ct
+      let c', ct = execute env c in
+      let cstr = if c == c' then cstr else mkProj (p,c') in
+      cstr, type_of_projection env p c' ct
 
     (* Lambda calculus operators *)
     | App (f,args) ->
-        let argst = execute_array env args in
-	let ft =
+      let args', argst = execute_array env args in
+        let f', ft =
 	  match kind f with
 	  | Ind ind when Environ.template_polymorphic_pind ind env ->
 	    let args = Array.map (fun t -> lazy t) argst in
-              type_of_inductive_knowing_parameters env ind args
+              f, type_of_inductive_knowing_parameters env ind args
 	  | _ ->
 	    (* No template polymorphism *)
             execute env f
 	in
-
-          type_of_apply env f ft args argst
+        let cstr = if f == f' && args == args' then cstr else mkApp (f',args') in
+        cstr, type_of_apply env f' ft args' argst
 
     | Lambda (name,c1,c2) ->
-      let s = execute_is_type env c1 in
-      check_binder_annot env s name;
-      let env1 = push_rel (LocalAssum (name,c1)) env in
-      let c2t = execute env1 c2 in
-        type_of_abstraction env name c1 c2t
+      let c1', s = execute_is_type env c1 in
+      let name' = check_binder_annot s name in
+      let env1 = push_rel (LocalAssum (name',c1')) env in
+      let c2', c2t = execute env1 c2 in
+      let cstr = if name == name' && c1 == c1' && c2 == c2' then cstr else mkLambda(name',c1',c2') in
+      cstr, type_of_abstraction env name' c1 c2t
 
     | Prod (name,c1,c2) ->
-      let vars = execute_is_type env c1 in
-      check_binder_annot env vars name;
-      let env1 = push_rel (LocalAssum (name,c1)) env in
-      let vars' = execute_is_type env1 c2 in
-        type_of_product env name vars vars'
+      let c1', vars = execute_is_type env c1 in
+      let name' = check_binder_annot vars name in
+      let env1 = push_rel (LocalAssum (name',c1')) env in
+      let c2', vars' = execute_is_type env1 c2 in
+      let cstr = if name == name' && c1 == c1' && c2 == c2' then cstr else mkProd(name',c1',c2') in
+      cstr, type_of_product env name' vars vars'
 
     | LetIn (name,c1,c2,c3) ->
-      let c1t = execute env c1 in
-      let c2s = execute_is_type env c2 in
-      check_binder_annot env c2s name;
-      let () = check_cast env c1 c1t DEFAULTcast c2 in
-      let env1 = push_rel (LocalDef (name,c1,c2)) env in
-      let c3t = execute env1 c3 in
-	subst1 c1 c3t
+      let c1', c1t = execute env c1 in
+      let c2', c2s = execute_is_type env c2 in
+      let name' = check_binder_annot c2s name in
+      let () = check_cast env c1' c1t DEFAULTcast c2' in
+      let env1 = push_rel (LocalDef (name',c1',c2')) env in
+      let c3', c3t = execute env1 c3 in
+      let cstr = if name == name' && c1 == c1' && c2 == c2' && c3 == c3' then cstr
+        else mkLetIn(name',c1',c2',c3')
+      in
+      cstr, subst1 c1 c3t
 
     | Cast (c,k,t) ->
-      let ct = execute env c in
-      let _ts = (check_type env t (execute env t)) in
-      let () = check_cast env c ct k t in
-	t
+      let c', ct = execute env c in
+      let t', _ts = execute_is_type env t in
+      let () = check_cast env c' ct k t' in
+      let cstr = if c == c' && t == t' then cstr else mkCast(c',k,t') in
+      cstr, t'
 
     (* Inductive types *)
     | Ind ind ->
-      type_of_inductive env ind
+      cstr, type_of_inductive env ind
 
     | Construct c ->
-      type_of_constructor env c
+      cstr, type_of_constructor env c
 
     | Case (ci,p,c,lf) ->
-        let ct = execute env c in
-        let pt = execute env p in
-        let lft = execute_array env lf in
-          type_of_case env ci p pt c ct lf lft
-
-    | Fix ((_vn,i as vni),recdef) ->
+        let c', ct = execute env c in
+        let p', pt = execute env p in
+        let lf', lft = execute_array env lf in
+        let ci', t = type_of_case env ci p' pt c' ct lf' lft in
+        let cstr = if ci == ci' && c == c' && p == p' && lf == lf' then cstr
+          else mkCase(ci',p',c',lf')
+        in
+        cstr, t
+
+    | Fix ((_vn,i as vni),recdef as fix) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
-      let fix = (vni,recdef') in
-        check_fix env fix; fix_ty
+      let cstr, fix = if recdef == recdef' then cstr, fix else
+          let fix = (vni,recdef') in mkFix fix, fix
+      in
+      check_fix env fix; cstr, fix_ty
 	  
-    | CoFix (i,recdef) ->
+    | CoFix (i,recdef as cofix) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
-      let cofix = (i,recdef') in
-        check_cofix env cofix; fix_ty
+      let cstr, cofix = if recdef == recdef' then cstr, cofix else
+          let cofix = (i,recdef') in mkCoFix cofix, cofix
+      in
+      check_cofix env cofix; cstr, fix_ty
 
     (* Primitive types *)
-    | Int _ -> type_of_int env
-	  
+    | Int _ -> cstr, type_of_int env
+
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
 	anomaly (Pp.str "the kernel does not support metavariables.")
@@ -576,18 +612,22 @@ let rec execute env cstr =
 	anomaly (Pp.str "the kernel does not support existential variables.")
 
 and execute_is_type env constr =
-  let t = execute env constr in
-    check_type env constr t
-
-and execute_recdef env (names,lar,vdef) i =
-  let lart = execute_array env lar in
-  let lara = Array.map3 (check_assumption env) names lar lart in
-  let env1 = push_rec_types (names,lara,vdef) env in
-  let vdeft = execute_array env1 vdef in
-  let () = check_fixpoint env1 names lara vdef vdeft in
-    (lara.(i),(names,lara,vdef))
-
-and execute_array env = Array.map (execute env)
+  let c, t = execute env constr in
+    c, check_type env constr t
+
+and execute_recdef env (names,lar,vdef as recdef) i =
+  let lar', lart = execute_array env lar in
+  let names' = Array.Smart.map_i (fun i na -> check_assumption env na lar'.(i) lart.(i)) names in
+  let env1 = push_rec_types (names',lar',vdef) env in (* vdef is ignored *)
+  let vdef', vdeft = execute_array env1 vdef in
+  let () = check_fixpoint env1 names' lar' vdef' vdeft in
+  let recdef = if names == names' && lar == lar' && vdef == vdef' then recdef else (names',lar',vdef') in
+    (lar'.(i),recdef)
+
+and execute_array env cs =
+  let tys = Array.make (Array.length cs) mkProp in
+  let cs = Array.Smart.map_i (fun i c -> let c, ty = execute env c in tys.(i) <- ty; c) cs in
+  cs, tys
 
 (* Derived functions *)
 
@@ -599,8 +639,8 @@ let check_wellformed_universes env c =
 
 let infer env constr =
   let () = check_wellformed_universes env constr in
-  let t = execute env constr in
-    make_judge constr t
+  let constr, t = execute env constr in
+  make_judge constr t
 
 let infer = 
   if Flags.profile then
@@ -617,30 +657,27 @@ let type_judgment env {uj_val=c; uj_type=t} =
 
 let infer_type env constr =
   let () = check_wellformed_universes env constr in
-  let t = execute env constr in
+  let constr, t = execute env constr in
   let s = check_type env constr t in
   {utj_val = constr; utj_type = s}
 
-let infer_v env cv =
-  let () = Array.iter (check_wellformed_universes env) cv in
-  let jv = execute_array env cv in
-    make_judgev cv jv
-
 (* Typing of several terms. *)
 
 let check_context env rels =
   let open Context.Rel.Declaration in
-  Context.Rel.fold_outside (fun d env ->
+  Context.Rel.fold_outside (fun d (env,rels) ->
     match d with
-      | LocalAssum (_,ty) ->
-        let _ = infer_type env ty in
-        push_rel d env
-      | LocalDef (_,bd,ty) ->
+      | LocalAssum (x,ty) ->
+        let jty = infer_type env ty in
+        let x = check_binder_annot jty.utj_type x in
+        push_rel d env, LocalAssum (x,jty.utj_val) :: rels
+      | LocalDef (x,bd,ty) ->
         let j1 = infer env bd in
-        let _ = infer_type env ty in
+        let jty = infer_type env ty in
         conv_leq false env j1.uj_type ty;
-        push_rel d env)
-    rels ~init:env
+        let x = check_binder_annot jty.utj_type x in
+        push_rel d env, LocalDef (x,j1.uj_val,jty.utj_val) :: rels)
+    rels ~init:(env,[])
 
 let judge_of_prop = make_judge mkProp type1
 let judge_of_set = make_judge mkSet type1
@@ -687,8 +724,8 @@ let judge_of_constructor env cu =
 
 let judge_of_case env ci pj cj lfj =
   let lf, lft = dest_judgev lfj in
-  make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft))
-             (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft)
+  let ci, t = type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft in
+  make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) t
 
 (* Building type of primitive operators and type *)
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index e57d6622c9..cc1885f42d 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -16,28 +16,28 @@ open Environ
 (** {6 Typing functions (not yet tagged as safe) }
 
     They return unsafe judgments that are "in context" of a set of
-    (local) universe variables (the ones that appear in the term)
-    and associated constraints. In case of polymorphic definitions,
-    these variables and constraints will be generalized.
- *)
+   (local) universe variables (the ones that appear in the term) and
+   associated constraints. In case of polymorphic definitions, these
+   variables and constraints will be generalized.
 
+    When typechecking a term it may be updated to fix relevance marks.
+   Do not discard the result. *)
 
 val infer      : env -> constr       -> unsafe_judgment
-val infer_v    : env -> constr array -> unsafe_judgment array
 val infer_type : env -> types        -> unsafe_type_judgment
 
 val check_context :
-  env -> Constr.rel_context -> env
+  env -> Constr.rel_context -> env * Constr.rel_context
 
 (** {6 Basic operations of the typing machine. } *)
 
 (** If [j] is the judgement {% $ %}c:t{% $ %}, then [assumption_of_judgement env j]
    returns the type {% $ %}c{% $ %}, checking that {% $ %}t{% $ %} is a sort. *)
 
-val assumption_of_judgment :  env -> unsafe_judgment -> types * Sorts.relevance
+val assumption_of_judgment :  env -> unsafe_judgment -> Sorts.relevance
 val type_judgment          :  env -> unsafe_judgment -> unsafe_type_judgment
 
-val check_binder_annot : env -> Sorts.t -> Name.t Context.binder_annot -> unit
+val check_binder_annot : Sorts.t -> Name.t Context.binder_annot -> Name.t Context.binder_annot
 
 (** {6 Type of sorts. } *)
 val type1 : types
@@ -130,3 +130,6 @@ val judge_of_int : env -> Uint63.t -> unsafe_judgment
 
 val type_of_prim_type : env -> CPrimitives.prim_type -> types
 val type_of_prim : env -> CPrimitives.t -> types
+
+val warn_bad_relevance_name : string
+(** Allow the checker to make this warning into an error. *)