diff options
| author | Gaëtan Gilbert | 2019-05-23 10:03:42 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-11 09:55:51 +0200 |
| commit | 82663b28a04d82e89bd041efd256c4838312e587 (patch) | |
| tree | 8f1c555626ebe40090143be1b663a0fe07377caf /interp/constrintern.ml | |
| parent | 45306c6c9c433b86406d041f58aafb7cf3a3ff82 (diff) | |
Simplify implicit_quantifiers
After removing `Instance : !type` implicit_application is only used in
constrintern. We propagate constant arguments ?allow_partial and
combine_params_freevar.
Also remove unused functions.
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1a81dc41a1..4c8aff3f2e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -392,9 +392,8 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars env {loc;v=na} b' t ty = let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in let ty, ids' = - if t then ty, ids else - Implicit_quantifiers.implicit_application ids - Implicit_quantifiers.combine_params_freevar ty + if t then ty, ids + else Implicit_quantifiers.implicit_application ids ty in let ty' = intern_type {env with ids = ids; unb = true} ty in let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in |