diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-07 18:57:37 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-07 18:57:37 +0000 |
| commit | 72994350da5ca5d11bfe545837500291c8da7732 (patch) | |
| tree | 859b16c3ff872c3660a18c3580705e8f2a594b99 /interp/constrintern.ml | |
| parent | 4c021bc57fda82fc97ae1e10768c8b59f6f85285 (diff) | |
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)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9616 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 9 |
1 files changed, 8 insertions, 1 deletions
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), [], [], [] |