diff options
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 5 |
1 files changed, 2 insertions, 3 deletions
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,_) = |