From fc60feb7a3ccd9ec88f6c46929f5fa8172bd7885 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 31 Jul 2019 13:32:25 +0200
Subject: Specialize the section API.

We split the function used to retrieve the local context from the one used to
provide the implicit status of each binder. Most of the users only rely on the
former indeed.
---
 interp/notation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index d88182241b..a78bc60e83 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1533,7 +1533,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) =
     let n =
       try
         let vars = Lib.variable_section_segment_of_reference r in
-        vars |> List.map fst |> List.filter is_local_assum |> List.length
+        vars |> List.filter is_local_assum |> List.length
       with
         Not_found (* Not a ref defined in this section *) -> 0 in
     Some (req,r,n,l,[])
-- 
cgit v1.2.3