diff options
| author | Pierre-Marie Pédrot | 2019-07-31 13:32:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-31 14:35:23 +0200 |
| commit | fc60feb7a3ccd9ec88f6c46929f5fa8172bd7885 (patch) | |
| tree | 309674e4e3debf44ca7c10b07e429f75022c9dd6 /interp/notation.ml | |
| parent | 162eefb562aca2c3741ec24d201deb881663e05a (diff) | |
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.
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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,[]) |