Fix bug #1959 (remember: never use a partial functions mindlessly).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11439 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 3 deletions

diff --git a/toplevel/record.ml b/toplevel/record.ml
index 8ac103fba..75a0c1293 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