aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-06-10 12:51:08 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-06-10 12:52:13 +0200
commitd192a84105a13f6c7fad376895a3569c1257a5d4 (patch)
tree3f49036a20ef187351d747069816ffe4bf6ffc0c
parent51a56b1aacb516af513de64c00dd7e796f661484 (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.ml14
-rw-r--r--test-suite/bugs/closed/7700.v9
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.