Remove the k0 argument from pretype functions.

This was introduced by @herbelin in
817308a, appears to have been
made unnecessary again by herbelin in
4dab4fc.

At this point it appears to be completely unused.

pretyping/pretyping.ml

@@ -380,7 +380,7 @@ let orelse_name name name' = match name with
   | Anonymous -> name'
   | _ -> name
 
-let pretype_id pretype k0 loc env sigma id =
+let pretype_id pretype loc env sigma id =
   (* Look for the binder of [id] *)
   try
     let (n,_,typ) = lookup_rel_id id (rel_context !!env) in
@@ -475,10 +475,10 @@ let mark_obligation_evar sigma k evc =
 (* in environment [env], with existential variables [sigma] and *)
 (* the type constraint tycon *)
 
-let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
+let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
   let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc in
-  let pretype_type = pretype_type ~program_mode ~poly k0 resolve_tc in
-  let pretype = pretype ~program_mode ~poly k0 resolve_tc in
+  let pretype_type = pretype_type ~program_mode ~poly resolve_tc in
+  let pretype = pretype ~program_mode ~poly resolve_tc in
   let open Context.Rel.Declaration in
   let loc = t.CAst.loc in
   match DAst.get t with
@@ -487,7 +487,7 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env
     inh_conv_coerce_to_tycon ?loc env sigma t_ref tycon
 
   | GVar id ->
-    let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) k0 loc env sigma id in
+    let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) loc env sigma id in
     inh_conv_coerce_to_tycon ?loc env sigma t_id tycon
 
   | GEvar (id, inst) ->
@@ -498,7 +498,7 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env
         try Evd.evar_key id sigma
         with Not_found -> error_evar_not_found ?loc !!env sigma id in
       let hyps = evar_filtered_context (Evd.find sigma evk) in
-      let sigma, args = pretype_instance ~program_mode ~poly k0 resolve_tc env sigma loc hyps evk inst in
+      let sigma, args = pretype_instance ~program_mode ~poly resolve_tc env sigma loc hyps evk inst in
       let c = mkEvar (evk, args) in
       let j = Retyping.get_judgment_of !!env sigma c in
       inh_conv_coerce_to_tycon ?loc env sigma j tycon
@@ -984,7 +984,7 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env
         in
         inh_conv_coerce_to_tycon ?loc env sigma resj tycon
 
-and pretype_instance ~program_mode ~poly k0 resolve_tc env sigma loc hyps evk update =
+and pretype_instance ~program_mode ~poly resolve_tc env sigma loc hyps evk update =
   let f decl (subst,update,sigma) =
     let id = NamedDecl.get_id decl in
     let b = Option.map (replace_vars subst) (NamedDecl.get_value decl) in
@@ -1016,7 +1016,7 @@ and pretype_instance ~program_mode ~poly k0 resolve_tc env sigma loc hyps evk up
     let sigma, c, update =
       try
         let c = List.assoc id update in
-        let sigma, c = pretype ~program_mode ~poly k0 resolve_tc (mk_tycon t) env sigma c in
+        let sigma, c = pretype ~program_mode ~poly resolve_tc (mk_tycon t) env sigma c in
         check_body sigma id (Some c.uj_val);
         sigma, c.uj_val, List.remove_assoc id update
       with Not_found ->
@@ -1041,7 +1041,7 @@ and pretype_instance ~program_mode ~poly k0 resolve_tc env sigma loc hyps evk up
   sigma, Array.map_of_list snd subst
 
 (* [pretype_type valcon env sigma c] coerces [c] into a type *)
-and pretype_type ~program_mode ~poly k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
+and pretype_type ~program_mode ~poly resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
   | GHole (knd, naming, None) ->
       let loc = loc_of_glob_constr c in
       (match valcon with
@@ -1068,7 +1068,7 @@ and pretype_type ~program_mode ~poly k0 resolve_tc valcon (env : GlobEnv.t) sigm
          let sigma = if program_mode then mark_obligation_evar sigma knd utj_val else sigma in
          sigma, { utj_val; utj_type = s})
   | _ ->
-      let sigma, j = pretype ~program_mode ~poly k0 resolve_tc empty_tycon env sigma c in
+      let sigma, j = pretype ~program_mode ~poly resolve_tc empty_tycon env sigma c in
       let loc = loc_of_glob_constr c in
       let sigma, tj = Coercion.inh_coerce_to_sort ?loc !!env sigma j in
 	match valcon with
@@ -1088,16 +1088,15 @@ let ise_pretype_gen flags env sigma lvar kind c =
     if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames
   in
   let env = GlobEnv.make ~hypnaming env sigma lvar in
-  let k0 = Context.Rel.length (rel_context !!env) in
   let sigma', c', c'_ty = match kind with
     | WithoutTypeConstraint ->
-      let sigma, j = pretype ~program_mode ~poly k0 flags.use_typeclasses empty_tycon env sigma c in
+      let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses empty_tycon env sigma c in
       sigma, j.uj_val, j.uj_type
     | OfType exptyp ->
-      let sigma, j = pretype ~program_mode ~poly k0 flags.use_typeclasses (mk_tycon exptyp) env sigma c in
+      let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses (mk_tycon exptyp) env sigma c in
       sigma, j.uj_val, j.uj_type
     | IsType ->
-      let sigma, tj = pretype_type ~program_mode ~poly k0 flags.use_typeclasses empty_valcon env sigma c in
+      let sigma, tj = pretype_type ~program_mode ~poly flags.use_typeclasses empty_valcon env sigma c in
       sigma, tj.utj_val, mkSort tj.utj_type
   in
   process_inference_flags flags !!env sigma (sigma',c',c'_ty)