diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-24 15:31:28 +0200 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-24 17:34:34 +0200 |
| commit | 663922262bc9bcc8876f7e12910f6294fc964753 (patch) | |
| tree | 9dab5db7e8741f0b2914fa390e8d0105a4bd06b2 /interp/notation.ml | |
| parent | 0591a05a40793e51604a3e9a68b4352099bd5333 (diff) | |
Changing the definition of the "Lib.variable.info" type to enable us to do more cleanups
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 0798d385d..3e3523d76 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,[]) |