diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 3 | ||||
| -rw-r--r-- | toplevel/record.ml | 5 | ||||
| -rw-r--r-- | toplevel/record.mli | 8 |
3 files changed, 8 insertions, 8 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 32803742a..4af59ff62 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -185,7 +185,8 @@ let declare_structure env id idbuild params arity fields = mind_entry_inds = [mie_ind] } in let kn = Command.declare_mutual_with_eliminations true mie in let rsp = (kn,0) in (* This is ind path of idstruc *) - let kinds,sp_projs = Record.declare_projections rsp (List.map (fun _ -> false) fields) fields in + let id = Nameops.next_ident_away id (ids_of_context (Global.env())) in + let kinds,sp_projs = Record.declare_projections rsp ~name:id (List.map (fun _ -> false) fields) fields in let _build = ConstructRef (rsp,1) in Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs); rsp diff --git a/toplevel/record.ml b/toplevel/record.ml index b94dffe1a..b04557304 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -131,15 +131,14 @@ let instantiate_possibly_recursive_type indsp paramdecls fields = substl_rel_context (subst@[mkInd indsp]) fields (* We build projections *) -let declare_projections indsp coers fields = +let declare_projections indsp ?name coers fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let paramdecls = mib.mind_params_ctxt in let r = mkInd indsp in let rp = applist (r, extended_rel_list 0 paramdecls) in let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*) - let x = Name (next_ident_away mip.mind_typename (ids_of_context (Global.env()))) in - (* Termops.named_hd (Global.env()) r Anonymous *) + let x = match name with Some n -> Name n | None -> Termops.named_hd (Global.env()) r Anonymous in let fields = instantiate_possibly_recursive_type indsp paramdecls fields in let lifted_fields = lift_rel_context 1 fields in let (_,kinds,sp_projs,_) = diff --git a/toplevel/record.mli b/toplevel/record.mli index e322dcfd0..5ba8b04e1 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -16,12 +16,12 @@ open Vernacexpr open Topconstr (*i*) -(* [declare_projections ref coers params fields] declare projections of - record [ref] (if allowed), and put them as coercions accordingly to - [coers]; it returns the absolute names of projections *) +(* [declare_projections ref name coers params fields] declare projections of + record [ref] (if allowed) using the given [name] as argument, and put them + as coercions accordingly to [coers]; it returns the absolute names of projections *) val declare_projections : - inductive -> bool list -> rel_context -> bool list * constant option list + inductive -> ?name:identifier -> bool list -> rel_context -> bool list * constant option list val definition_structure : lident with_coercion * local_binder list * |