diff options
| -rw-r--r-- | toplevel/record.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 8ac103fba1..75a0c12938 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -38,16 +38,20 @@ let interp_evars evdref env ?(impls=([],[])) k typ = let mk_interning_data env na impls typ = let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls - in (out_name na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ)) + in (na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ)) let interp_fields_evars isevars env l = List.fold_left (fun (env, uimpls, params, impls) ((loc, i), b, t) -> let impl, t' = interp_evars isevars env ~impls Pretyping.IsType t in let b' = Option.map (fun x -> snd (interp_evars isevars env ~impls (Pretyping.OfType (Some t')) x)) b in - let data = mk_interning_data env i impl t' in + let impls = + match i with + | Anonymous -> impls + | Name na -> (fst impls, mk_interning_data env na impl t' :: snd impls) + in let d = (i,b',t') in - (push_rel d env, impl :: uimpls, d::params, ([], data :: snd impls))) + (push_rel d env, impl :: uimpls, d::params, impls)) (env, [], [], ([], [])) l let binder_of_decl = function |