1 files changed, 16 insertions, 18 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 6ce14c853..2eb2c040e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -20,7 +20,9 @@ open Declarations
 open Environ
 open Entries
 open Typeops
-open Fast_typeops
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
 
 (* Insertion of constants and parameters in environment. *)
 
@@ -95,8 +97,7 @@ let inline_side_effects env body ctx side_eff =
     let cbl = List.filter not_exists cbl in
     let cname c = 
       let name = string_of_con c in
-      for i = 0 to String.length name - 1 do
-        if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done;
+      let name = String.map (fun c -> if c == '.' || c == '#' then '_' else c) name in
       Name (id_of_string name) in
     let rec sub c i x = match kind_of_term x with
       | Const (c', _) when eq_constant c c' -> mkRel i
@@ -214,7 +215,7 @@ let infer_declaration ~trust env kn dcl =
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
-        Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) ->
+        Future.chain ~pure:true body (fun ((body,uctx),side_eff) ->
           let body, uctx, signatures =
             inline_side_effects env body uctx side_eff in
           let valid_signatures = check_signatures trust signatures in
@@ -286,18 +287,17 @@ let global_vars_set_constant_type env = function
   | RegularArity t -> global_vars_set env t
   | TemplateArity (ctx,_) ->
       Context.Rel.fold_outside
-        (Context.Rel.Declaration.fold
+        (RelDecl.fold_constr
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
 let record_aux env s_ty s_bo suggested_expr =
-  let open Context.Named.Declaration in
   let in_ty = keep_hyps env s_ty in
   let v =
     String.concat " "
       (CList.map_filter (fun decl ->
-          let id = get_id decl in
-          if List.exists (Id.equal id % get_id) in_ty then None
+          let id = NamedDecl.get_id decl in
+          if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None
           else Some (Id.to_string id))
         (keep_hyps env s_bo)) in
   Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
@@ -306,26 +306,25 @@ let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
 let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
-  let open Context.Named.Declaration in
   let check declared inferred =
-    let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in
+    let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
     if not (Id.Set.subset inferred_set declared_set) then
       let l = Id.Set.elements (Idset.diff inferred_set declared_set) in
       let n = List.length l in
-      errorlabstrm "" (Pp.(str "The following section " ++
+      user_err  (Pp.(str "The following section " ++
         str (String.plural n "variable") ++
         str " " ++ str (String.conjugate_verb_to_be n) ++
         str " used but not declared:" ++
         fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in
   let sort evn l =
     List.filter (fun decl ->
-      let id = get_id decl in
-      List.exists (Names.Id.equal id % get_id) l)
+      let id = NamedDecl.get_id decl in
+      List.exists (NamedDecl.get_id %> Names.Id.equal id) l)
     (named_context env) in
   (* We try to postpone the computation of used section variables *)
   let hyps, def =
-    let context_ids = List.map get_id (named_context env) in
+    let context_ids = List.map NamedDecl.get_id (named_context env) in
     match ctx with
     | None when not (List.is_empty context_ids) -> 
         (* No declared section vars, and non-empty section context:
@@ -453,7 +452,7 @@ let export_side_effects mb env ce =
       let { const_entry_body = body } = c in
       let _, eff = Future.force body in
       let ce = DefinitionEntry { c with
-        const_entry_body = Future.chain ~greedy:true ~pure:true body
+        const_entry_body = Future.chain ~pure:true body
           (fun (b_ctx, _) -> b_ctx, empty_seff) } in
       let not_exists (c,_,_,_) =
         try ignore(Environ.lookup_constant c env); false
@@ -519,8 +518,7 @@ let translate_local_def mb env id centry =
     | Undef _ -> ()
     | Def _ -> ()
     | OpaqueDef lc ->
-       let open Context.Named.Declaration in
-       let context_ids = List.map get_id (named_context env) in
+       let context_ids = List.map NamedDecl.get_id (named_context env) in
        let ids_typ = global_vars_set env typ in
        let ids_def = global_vars_set env
          (Opaqueproof.force_proof (opaque_tables env) lc) in
@@ -536,7 +534,7 @@ let translate_local_def mb env id centry =
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
 let inline_entry_side_effects env ce = { ce with
-  const_entry_body = Future.chain ~greedy:true ~pure:true
+  const_entry_body = Future.chain ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
       let body, ctx',_ = inline_side_effects env body ctx side_eff in
       (body, ctx'), empty_seff);