Merge PR#552: Miscelaneous commits

8 files changed, 21 insertions, 46 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 9c264439b..f054038e9 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1020,11 +1020,11 @@ module Goal = struct
 
   let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t)
 
-  let env { env=env } = env
-  let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma
-  let hyps { env=env } = EConstr.named_context env
-  let concl { concl=concl } = concl
-  let extra { sigma=sigma; self=self } = goal_extra sigma self
+  let env {env} = env
+  let sigma {sigma} = Sigma.Unsafe.of_evar_map sigma
+  let hyps {env} = EConstr.named_context env
+  let concl {concl} = concl
+  let extra {sigma; self} = goal_extra sigma self
 
   let gmake_with info env sigma goal = 
     { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
@@ -1040,7 +1040,7 @@ module Goal = struct
   let nf_enter f =
     InfoL.tag (Info.Dispatch) begin
     iter_goal begin fun goal ->
-      Env.get >>= fun env ->
+      tclENV >>= fun env ->
       tclEVARMAP >>= fun sigma ->
       try
         let (gl, sigma) = nf_gmake env sigma goal in
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 5ba26d828..1facb47e1 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -19,7 +19,7 @@ open Util
 (** [find_reference caller_message [dir;subdir;...] s] returns a global
    reference to the name dir.subdir.(...).s; the corresponding module
    must have been required or in the process of being compiled so that
-   it must be used lazyly; it raises an anomaly with the given message
+   it must be used lazily; it raises an anomaly with the given message
    if not found *)
 
 type message = string
diff --git a/kernel/context.mli b/kernel/context.mli
index 0c666a25d..24e69ebd6 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 7821ea20f..71e228b19 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 ee8d838da..5c10badbe 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 d14a254d3..48d7ee9ec 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)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5af0e1d9b..e4a87739b 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1221,7 +1221,7 @@ open Decl_kinds
         | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
         | [], [] -> []
         | _ -> assert false in
-      hov 1 (pr_sequence (fun x -> x) (aux rl cl))
+      hov 1 (pr_sequence identity (aux rl cl))
     with Not_found ->
       hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 61b776f24..5f4a7766f 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -88,7 +88,7 @@ type proof_terminator = proof_ending -> unit
 type closed_proof = proof_object * proof_terminator
 
 type pstate = {
-  pid : Id.t;
+  pid : Id.t;  (* the name of the theorem whose proof is being constructed *)
   terminator : proof_terminator CEphemeron.key;
   endline_tactic : Genarg.glob_generic_argument option;
   section_vars : Context.Named.t option;