Renaming variants of Entries.local_entry

The original datatype:

  Entries.local_entry = LocalDef of constr
                      | LocalAssum of constr

was changed to:

  Entries.local_entry = LocalDefEntry of constr
                      | LocalAssumEntry of constr

There are two advantages:

  1. the new names are consistent with other variant names in the same module
     which also have this "*Entry" suffix
  2. the new names do not collide with variants defined in the Context.{Rel,Named}.Declaration
     modules so both, "Entries" as well as "Context.{Rel,Named}.Declaration" can be open at the same time.

The disadvantage is that those new variants are longer.
But since those variants are rarely used, it it is not a big deal.

5 files changed, 17 insertions, 16 deletions

diff --git a/kernel/entries.mli b/kernel/entries.mli
index b2a77dd950..3ecfcca64c 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -18,8 +18,8 @@ open Term
 (** {6 Local entries } *)
 
 type local_entry =
-  | LocalDef of constr
-  | LocalAssum of constr
+  | LocalDefEntry of constr
+  | LocalAssumEntry of constr
 
 
 (** {6 Declaration of inductive types. } *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index eeb12a2b49..0ea68e2bcc 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -18,6 +18,7 @@ open Entries
 open Reduction
 open Inductive
 open Type_errors
+open Context.Rel.Declaration
 
 let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y
 
@@ -77,7 +78,6 @@ let judge_of_type u =
 (*s Type of a de Bruijn index. *)
 
 let judge_of_relative env n =
-  let open Context.Rel.Declaration in
   try
     let typ = get_type (lookup_rel n env) in
     { uj_val  = mkRel n;
@@ -99,9 +99,9 @@ let judge_of_variable env id =
    variables of the current env.
    Order does not have to be checked assuming that all names are distinct *)
 let check_hyps_inclusion env c sign =
-  let open Context.Named.Declaration in
   Context.Named.fold_outside
     (fun d1 () ->
+      let open Context.Named.Declaration in
       let id = get_id d1 in
       try
         let d2 = lookup_named id env in
@@ -127,7 +127,6 @@ let extract_level env p =
   match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None
 
 let extract_context_levels env l =
-  let open Context.Rel.Declaration in
   let fold l = function
     | LocalAssum (_,p) -> extract_level env p :: l
     | LocalDef _ -> l
@@ -420,7 +419,6 @@ let type_fixpoint env lna lar vdefj =
     Ind et Constructsi un jour cela devient des constructions
     arbitraires et non plus des variables *)
 let rec execute env cstr =
-  let open Context.Rel.Declaration in
   match kind_of_term cstr with
     (* Atomic terms *)
     | Sort (Prop c) ->
@@ -553,12 +551,12 @@ let infer_v env cv =
 (* Typing of several terms. *)
 
 let infer_local_decl env id = function
-  | LocalDef c ->
+  | LocalDefEntry c ->
       let j = infer env c in
-      Context.Rel.Declaration.LocalDef (Name id, j.uj_val, j.uj_type)
-  | LocalAssum c ->
+      LocalDef (Name id, j.uj_val, j.uj_type)
+  | LocalAssumEntry c ->
       let j = infer env c in
-      Context.Rel.Declaration.LocalAssum (Name id, assumption_of_judgment env j)
+      LocalAssum (Name id, assumption_of_judgment env j)
 
 let infer_local_decls env decls =
   let rec inferec env = function
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 166fe94ead..284bcd75ec 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -38,6 +38,7 @@ open Misctypes
 open Vernacexpr
 open Sigma.Notations
 open Context.Rel.Declaration
+open Entries
 
 let do_universe poly l = Declare.do_universe poly l
 let do_constraint poly l = Declare.do_constraint poly l
@@ -385,8 +386,8 @@ let mk_mltype_data evdref env assums arity indname =
   (is_ml_type,indname,assums)
 
 let prepare_param = function
-  | LocalAssum (na,t) -> out_name na, Entries.LocalAssum t
-  | LocalDef (na,b,_) -> out_name na, Entries.LocalDef b
+  | LocalAssum (na,t) -> out_name na, LocalAssumEntry t
+  | LocalDef (na,b,_) -> out_name na, LocalDefEntry b
 
 (** Make the arity conclusion flexible to avoid generating an upper bound universe now,
     only if the universe does not appear anywhere else.
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 5fa51e06e4..ffa11679c2 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -14,6 +14,7 @@ open Vars
 open Entries
 open Declarations
 open Cooking
+open Entries
 open Context.Rel.Declaration
 
 (********************************)
@@ -21,8 +22,8 @@ open Context.Rel.Declaration
 
 let detype_param =
   function
-  | LocalAssum (Name id, p) -> id, Entries.LocalAssum p
-  | LocalDef (Name id, p,_) -> id, Entries.LocalDef p
+  | LocalAssum (Name id, p) -> id, LocalAssumEntry p
+  | LocalDef (Name id, p,_) -> id, LocalDefEntry p
   | _ -> anomaly (Pp.str "Unnamed inductive local variable")
 
 (* Replace
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 4cf81a250c..c0bb9eb86c 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -26,6 +26,7 @@ open Constrexpr_ops
 open Goptions
 open Sigma.Notations
 open Context.Rel.Declaration
+open Entries
 
 (********** definition d'un record (structure) **************)
 
@@ -164,8 +165,8 @@ let degenerate_decl decl =
     | Name id -> id
     | Anonymous -> anomaly (Pp.str "Unnamed record variable") in
   match decl with
-    | LocalAssum (_,t) -> (id, Entries.LocalAssum t)
-    | LocalDef (_,b,_) -> (id, Entries.LocalDef b)
+    | LocalAssum (_,t) -> (id, LocalAssumEntry t)
+    | LocalDef (_,b,_) -> (id, LocalDefEntry b)
 
 type record_error =
   | MissingProj of Id.t * Id.t list