From 72994350da5ca5d11bfe545837500291c8da7732 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 7 Feb 2007 18:57:37 +0000 Subject: Correction bug #1364 (les variables de section sont repérées par interp_var : ne pas les repérer à nouveau comme objets globaux, puisqu'elles ont pu être effacées dans un contexte local de but). (report revision 9611 de la branche 8.1 vers le trunk) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9616 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/constrintern.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 64637bd09..0a42d2ba9 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -292,6 +292,12 @@ let intern_qualid loc qid = with Not_found -> error_global_not_found_loc loc qid +(* Rule out section vars since these should have been found by intern_var *) +let intern_non_secvar_qualid loc qid = + match intern_qualid loc qid with + | RRef (loc, VarRef id) -> error_global_not_found_loc loc qid + | r -> r + let intern_inductive r = let loc,qid = qualid_of_reference r in try match Nametab.extended_locate qid with @@ -312,7 +318,8 @@ let intern_reference env lvar = function | Ident (loc, id) -> try intern_var env lvar loc id with Not_found -> - try find_appl_head_data lvar (intern_qualid loc (make_short_qualid id)) + let qid = make_short_qualid id in + try find_appl_head_data lvar (intern_non_secvar_qualid loc qid) with e -> (* Extra allowance for non globalizing functions *) if !interning_grammar then RVar (loc,id), [], [], [] -- cgit v1.2.3