From d192a84105a13f6c7fad376895a3569c1257a5d4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
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