From 6df4e0fe6bc6076bc95a1a71d28ae049d04ba517 Mon Sep 17 00:00:00 2001 From: pboutill Date: Thu, 10 Feb 2011 14:11:01 +0000 Subject: Data structure telling implicits of local variables is a map in the intern_env git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13823 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/record.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'toplevel') diff --git a/toplevel/record.ml b/toplevel/record.ml index 27b6ffabe..74a33f6f9 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -41,12 +41,12 @@ let interp_fields_evars evars env nots l = let impls = match i with | Anonymous -> impls - | Name id -> (id, compute_internalization_data env Constrintern.Method t' impl) :: impls + | Name id -> Idmap.add id (compute_internalization_data env Constrintern.Method t' impl) impls in let d = (i,b',t') in List.iter (Metasyntax.set_notation_for_interpretation impls) no; (push_rel d env, impl :: uimpls, d::params, impls)) - (env, [], [], []) nots l + (env, [], [], empty_internalization_env) nots l let binder_of_decl = function | Vernacexpr.AssumExpr(n,t) -> (n,None,t) -- cgit v1.2.3