diff options
| author | Gaëtan Gilbert | 2020-09-30 12:25:02 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-06 12:40:33 +0200 |
| commit | c8c1723747c7e0eb748861cc12aecca411848f4c (patch) | |
| tree | d3e62beaa23ca07f199ca3f0928c87511f1ba19e /interp/implicit_quantifiers.ml | |
| parent | 6d3a9220204de22e0b81dc961d2eb269128b5c2e (diff) | |
First list in cl_context is just booleans
Used only by implicit_quantifiers
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 4016a3600e..c5324702dc 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -150,12 +150,12 @@ let combine_params avoid applied needed = | app, (_, (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, (None, (LocalAssum ({binder_name=Name id}, _))) :: need -> + | (x, None) :: app, (false, (LocalAssum ({binder_name=Name id}, _))) :: need -> aux (x :: ids) avoid app need - | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need + | x :: app, (false, _) :: need -> aux (fst x :: ids) avoid app need - | _, (Some _, decl) :: need | [], (None, 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 |