diff options
| author | Gaëtan Gilbert | 2020-09-30 12:32:31 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-06 12:40:35 +0200 |
| commit | 661d84228fa1a6750b4a80f41c3e012e6de763bf (patch) | |
| tree | 0f0e9dba77310071bcc51c92c92d99dd6f3c9239 | |
| parent | c8c1723747c7e0eb748861cc12aecca411848f4c (diff) | |
Simplify Implicit_quantifiers.combine_params a bit
| -rw-r--r-- | interp/implicit_quantifiers.ml | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index c5324702dc..0ed0b8a1a5 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -127,10 +127,7 @@ let combine_params avoid applied needed = List.partition (function (t, Some {CAst.loc;v=ExplByName id}) -> - let is_id (_, decl) = match RelDecl.get_name decl with - | Name id' -> Id.equal id id' - | Anonymous -> false - in + let is_id (_, decl) = Name.equal (Name id) (RelDecl.get_name decl) in if not (List.exists is_id needed) then user_err ?loc (str "Wrong argument name: " ++ Id.print id); true @@ -147,15 +144,13 @@ let combine_params avoid applied needed = | [], [] -> List.rev ids, avoid - | app, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named -> + | _, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named -> aux (Id.List.assoc id named :: ids) avoid app need - | (x, None) :: app, (false, (LocalAssum ({binder_name=Name id}, _))) :: need -> - aux (x :: ids) avoid app need + | (x, _) :: app, (false, _) :: need -> aux (x :: ids) avoid app need - | x :: app, (false, _) :: need -> aux (fst x :: ids) avoid app need - - | _, (true, decl) :: need | [], (false, decl) :: need -> + | _, (true, decl) :: need + | [], (false, decl) :: need -> let id' = next_name_away_from (RelDecl.get_name decl) avoid in let t' = CAst.make @@ CRef (qualid_of_ident id',None) in aux (t' :: ids) (Id.Set.add id' avoid) app need |