diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-10 12:51:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-10 12:52:13 +0200 |
| commit | d192a84105a13f6c7fad376895a3569c1257a5d4 (patch) | |
| tree | 3f49036a20ef187351d747069816ffe4bf6ffc0c | |
| parent | 51a56b1aacb516af513de64c00dd7e796f661484 (diff) | |
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.
| -rw-r--r-- | interp/constrintern.ml | 14 | ||||
| -rw-r--r-- | test-suite/bugs/closed/7700.v | 9 |
2 files changed, 14 insertions, 9 deletions
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. |