From d192a84105a13f6c7fad376895a3569c1257a5d4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 10 Jun 2018 12:51:08 +0200 Subject: Fixing #7700 (section variables bound to abbreviations were not found). Redundancy between finding section variables in both interp_var and interp_qualid could probably be cleaned. --- interp/constrintern.ml | 14 +++++--------- test-suite/bugs/closed/7700.v | 9 +++++++++ 2 files changed, 14 insertions(+), 9 deletions(-) create mode 100644 test-suite/bugs/closed/7700.v diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 848180743..e09b7a793 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -994,9 +994,12 @@ let glob_sort_of_level (level: glob_level) : glob_sort = | GType info -> GType [sort_info_of_level_info info] (* Is it a global reference or a syntactic definition? *) -let intern_qualid qid intern env ntnvars us args = +let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let loc = qid.loc in match intern_extended_global_of_qualid qid with + | TrueGlobal (VarRef _) when no_secvar -> + (* Rule out section vars since these should have been found by intern_var *) + raise Not_found | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args | SynDef sp -> let (ids,c) = Syntax_def.search_syntactic_definition ?loc sp in @@ -1033,13 +1036,6 @@ let intern_qualid qid intern env ntnvars us args = in c, projapp, args2 -(* Rule out section vars since these should have been found by intern_var *) -let intern_non_secvar_qualid qid intern env ntnvars us args = - let c, _, _ as r = intern_qualid qid intern env ntnvars us args in - match DAst.get c with - | GRef (VarRef _, _) -> raise Not_found - | _ -> r - let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function | {loc; v=Qualid qid} -> @@ -1055,7 +1051,7 @@ function with Not_found -> let qid = make ?loc @@ qualid_of_ident id in try - let r, projapp, args2 = intern_non_secvar_qualid qid intern env ntnvars us args in + let r, projapp, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 with Not_found -> diff --git a/test-suite/bugs/closed/7700.v b/test-suite/bugs/closed/7700.v new file mode 100644 index 000000000..56f5481ba --- /dev/null +++ b/test-suite/bugs/closed/7700.v @@ -0,0 +1,9 @@ +(* Abbreviations to section variables were not located *) +Section foo. + Let x := Set. + Notation y := x. + Check y. + Variable x' : Set. + Notation y' := x'. + Check y'. +End foo. -- cgit v1.2.3