diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 6 | ||||
| -rw-r--r-- | interp/notation.ml | 5 |
2 files changed, 8 insertions, 3 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 10cfbe58f..4d9386b9d 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -21,6 +21,8 @@ open Libobject open Nameops open Misctypes open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (*i*) let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" @@ -198,7 +200,7 @@ let combine_params avoid fn applied needed = List.partition (function (t, Some (loc, ExplByName id)) -> - let is_id (_, decl) = match get_name decl with + let is_id (_, decl) = match RelDecl.get_name decl with | Name id' -> Id.equal id id' | Anonymous -> false in @@ -242,7 +244,7 @@ let combine_params avoid fn applied needed = let combine_params_freevar = fun avoid (_, decl) -> - let id' = next_name_away_from (get_name decl) avoid in + let id' = next_name_away_from (RelDecl.get_name decl) avoid in (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid) let destClassApp cl = diff --git a/interp/notation.ml b/interp/notation.ml index 0798d385d..6279622bf 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -20,6 +20,9 @@ open Notation_term open Glob_term open Glob_ops open Ppextend +open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (*i*) (*s A scope is a set of notations; it includes @@ -686,7 +689,7 @@ 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) + 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,[]) |