golfing and doc in structures.ml*

engine/evd.ml

@@ -892,12 +892,8 @@ let mem d e = EvMap.mem e d.undf_evars || EvMap.mem e d.defn_evars
 
 let undefined_map d = d.undf_evars
 
-let undefined_evars d = EvMap.domain d.undf_evars
-
 let defined_map d = d.defn_evars
 
-let defined_evars d = EvMap.domain d.defn_evars
-
 let drop_all_defined d = { d with defn_evars = EvMap.empty }
 
 (* spiwack: not clear what folding over an evar_map, for now we shall

engine/evd.mli

@@ -276,15 +276,9 @@ val add_quconstraints : evar_map -> Sorts.QUConstraints.t -> evar_map
 val undefined_map : evar_map -> undefined evar_info Evar.Map.t
 (** Access the undefined evar mapping directly. *)
 
-val undefined_evars : evar_map -> Evar.Set.t
-(** Access the set of undefined evars. *)
-
 val defined_map : evar_map -> defined evar_info Evar.Map.t
 (** Access the defined evar mapping directly. *)
 
-val defined_evars : evar_map -> Evar.Set.t
-(** Access the set of defined evars. *)
-
 val drop_all_defined : evar_map -> evar_map
 
 val drop_new_defined : original:evar_map -> evar_map -> evar_map

pretyping/structures.ml

@@ -99,7 +99,8 @@ let is_projection cst = Cmap.mem cst !projection_table
 
 let projection_number env cst =
   let s = find_from_projection cst in
-  CList.index (Option.equal (Environ.QConstant.equal env)) (Some cst) (List.map (fun x -> x.proj_body) s.projections) - 1
+  CList.index0 (Option.equal (Environ.QConstant.equal env)) (Some cst)
+    (List.map (fun x -> x.proj_body) s.projections)
 
 end
 

pretyping/structures.mli

@@ -54,6 +54,8 @@ val projection_nparams : Names.Constant.t -> int
 val is_projection : Names.Constant.t -> bool
 
 val projection_number : Environ.env -> Names.Constant.t -> int
+(** [projection_number env p] returns the position of the projection p in
+    the structure it corresponds to, counting from 0. *)
 
 end