From 7f8fb01ffcaa6aeafef0cea9d7169d70ce841537 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 8 Oct 2008 18:06:28 +0000
Subject: 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
---
 toplevel/record.ml | 10 +++++++---
 1 file 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
-- 
cgit v1.2.3