From 663922262bc9bcc8876f7e12910f6294fc964753 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 24 Aug 2016 15:31:28 +0200
Subject: Changing the definition of the "Lib.variable.info" type to enable us
 to do more cleanups

---
 interp/notation.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/notation.ml b/interp/notation.ml
index 0798d385d4..3e3523d76a 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -686,7 +686,8 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) =
     let n =
       try
         let vars = Lib.variable_section_segment_of_reference r in
-        List.length (List.filter (fun (_,_,b,_) -> b = None) vars)
+        let open Context.Named.Declaration in
+        vars |> List.map fst |> List.filter is_local_assum |> List.length
       with
         Not_found (* Not a ref defined in this section *) -> 0 in
     Some (req,Lib.discharge_global r,n,l,[])
-- 
cgit v1.2.3