Merge PR#552: Miscelaneous commits

4 files changed, 12 insertions, 37 deletions

diff --git a/kernel/context.mli b/kernel/context.mli
index 0c666a25d9..24e69ebd6e 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -214,7 +214,7 @@ sig
     val to_rel_decl : ('c, 't) pt -> ('c, 't) Rel.Declaration.pt
   end
 
-  (** Rel-context is represented as a list of declarations.
+  (** Named-context is represented as a list of declarations.
       Inner-most declarations are at the beginning of the list.
       Outer-most declarations are at the end of the list. *)
   type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list
@@ -223,7 +223,7 @@ sig
   (** empty named-context *)
   val empty : ('c, 't) pt
 
-  (** Return a new rel-context enriched by with a given inner-most declaration. *)
+  (** Return a new named-context enriched by with a given inner-most declaration. *)
   val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt
 
   (** Return the number of {e local declarations} in a given named-context. *)
@@ -233,7 +233,7 @@ sig
       @raise Not_found if the designated identifier is not bound in a given named-context. *)
   val lookup : Id.t -> ('c, 't) pt -> ('c, 't) Declaration.pt
 
-  (** Check whether given two rel-contexts are equal. *)
+  (** Check whether given two named-contexts are equal. *)
   val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool
 
   (** Map all terms in a given named-context. *)
@@ -253,8 +253,8 @@ sig
   (** Return the set of all identifiers bound in a given named-context. *)
   val to_vars : ('c, 't) pt -> Id.Set.t
 
-  (** [instance_from_named_context Ω] builds an instance [args] such
-      that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
+  (** [to_instance Ω] builds an instance [args] such
+      that [Ω ⊢ args:Ω] where [Ω] is a named-context and with the local
       definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
       gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
   val to_instance : (Id.t -> 'r) -> ('c, 't) pt -> 'r list
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 7821ea20ff..71e228b19c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -77,7 +77,7 @@ type typing_flags = {
 }
 
 (* some contraints are in constant_constraints, some other may be in
- * the OpaueDef *)
+ * the OpaqueDef *)
 type constant_body = {
     const_hyps : Context.Named.t; (** New: younger hyp at top *)
     const_body : constant_def;
diff --git a/kernel/names.ml b/kernel/names.ml
index ee8d838da1..5c10badbec 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -162,21 +162,8 @@ module DirPath =
 struct
   type t = module_ident list
 
-  let rec compare (p1 : t) (p2 : t) =
-    if p1 == p2 then 0
-    else begin match p1, p2 with
-    | [], [] -> 0
-    | [], _ -> -1
-    | _, [] -> 1
-    | id1 :: p1, id2 :: p2 ->
-      let c = Id.compare id1 id2 in
-      if Int.equal c 0 then compare p1 p2 else c
-    end
-
-  let rec equal p1 p2 = p1 == p2 || match p1, p2 with
-  | [], [] -> true
-  | id1 :: p1, id2 :: p2 -> Id.equal id1 id2 && equal p1 p2
-  | _ -> false
+  let compare = List.compare Id.compare
+  let equal = List.equal Id.equal
 
   let rec hash accu = function
   | [] -> accu
@@ -191,7 +178,7 @@ struct
 
   let empty = []
 
-  let is_empty d = match d with [] -> true | _ -> false
+  let is_empty = List.is_empty
 
   let to_string = function
     | [] -> "<>"
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index d14a254d32..48d7ee9ec3 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -68,8 +68,8 @@ type named_context_val = {
 }
 
 type env = {
-  env_globals       : globals;
-  env_named_context : named_context_val;
+  env_globals       : globals;           (* globals = constants + inductive types + modules + module-types *)
+  env_named_context : named_context_val; (* section variables *)
   env_rel_context   : Context.Rel.t;
   env_rel_val       : lazy_val list;
   env_nb_rel        : int;
@@ -161,19 +161,7 @@ let map_named_val f ctxt =
   else { env_named_ctx = ctx; env_named_map = map }
 
 let push_named d env =
-(*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
-  assert (env.env_rel_context = []); *)
-  { env_globals = env.env_globals;
-    env_named_context = push_named_context_val d env.env_named_context;
-    env_rel_context = env.env_rel_context;
-    env_rel_val = env.env_rel_val;
-    env_nb_rel = env.env_nb_rel;
-    env_stratification = env.env_stratification;
-    env_typing_flags = env.env_typing_flags;
-    env_conv_oracle = env.env_conv_oracle;
-    retroknowledge = env.retroknowledge;
-    indirect_pterms = env.indirect_pterms;
-  }
+  {env with env_named_context = push_named_context_val d env.env_named_context}
 
 let lookup_named id env =
   fst (Id.Map.find id env.env_named_context.env_named_map)