From 7678cf243d054b620ba78926f2effb4dd97f0bdc Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 2 Feb 2017 11:17:02 +0100
Subject: refactoring "Names.DirPath.equal" function

---
 kernel/names.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index ee8d838da1..da02a32a28 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -173,10 +173,7 @@ struct
       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 equal = List.equal Id.equal
 
   let rec hash accu = function
   | [] -> accu
-- 
cgit v1.2.3


From 2198b0b28a396377ed8f885eddf6bc752af9c580 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 2 Feb 2017 11:18:26 +0100
Subject: refactoring "Names.DirPath.compare" function

---
 kernel/names.ml | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index da02a32a28..b91fa758f9 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -162,17 +162,7 @@ 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 compare = List.compare Id.compare
   let equal = List.equal Id.equal
 
   let rec hash accu = function
-- 
cgit v1.2.3


From dda06512833eea2805a8406b407494014371b2be Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 2 Feb 2017 11:20:51 +0100
Subject: refactoring "Names.DirPath.is_empty" function

---
 kernel/names.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index b91fa758f9..5c10badbec 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -178,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
     | [] -> "<>"
-- 
cgit v1.2.3


From 207ec95b8bda34e4c905e07a1ec6462c5fdefdb0 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 2 Feb 2017 14:35:51 +0100
Subject: simplifying "Environ.push_named" function

---
 kernel/pre_env.ml | 14 +-------------
 1 file changed, 1 insertion(+), 13 deletions(-)

(limited to 'kernel')

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index d14a254d32..6bfba2d40b 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -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)
-- 
cgit v1.2.3


From 4fc8616852438e80b10e0247550cc8968d76e9d7 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 9 Feb 2017 18:33:56 +0100
Subject: correcting comments in the "Context" module

---
 kernel/context.mli | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3


From aaf20df2f9e531f1f05fbf72de796f9761cd646b Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 2 Feb 2017 10:04:16 +0100
Subject: correcting a typo in a comment

---
 kernel/declarations.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

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;
-- 
cgit v1.2.3


From 40f7eb94b653b60f79c4f6eb204960037fcffa66 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 7 Nov 2016 14:41:52 +0100
Subject: COMMENT: Pre_env.env

---
 kernel/pre_env.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 6bfba2d40b..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;
-- 
cgit v1.2.3