diff options
| author | Gaëtan Gilbert | 2019-05-16 14:21:37 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-16 15:39:45 +0200 |
| commit | 21269d0fef6794a672c36abdc5760889adc0e09c (patch) | |
| tree | 13a76dc747db29bb9d21702363dba030f7c9be19 /interp/implicit_quantifiers.ml | |
| parent | 4197f42c15f0116eeb58df5b64b60f2fa6f6951f (diff) | |
binder_kind Generalized: remove 1st arg as it's always Implicit
https://coq.inria.fr/distrib/current/refman/language/gallina-extensions.html#implicit-generalization
>The generalizing binders `{ } and `( ) work similarly to their
>explicit counterparts, only binding the generalized variables
>implicitly, as maximally-inserted arguments.
I guess this was meant to provide a way to get "(A:_) {B:bla A}" from
"`{B:bla A}" (where A is generalizable) but there's no syntax for it
so let's drop the ml side until such a syntax exists.
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 8d45290ac0..f71ad14dd4 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -196,10 +196,9 @@ let combine_params avoid fn applied needed = user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments") in aux [] avoid applied needed -let combine_params_freevar = - fun avoid (_, decl) -> - let id' = next_name_away_from (RelDecl.get_name decl) avoid in - (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid) +let combine_params_freevar avoid (_, decl) = + let id' = next_name_away_from (RelDecl.get_name decl) avoid in + (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid) let destClassApp cl = let open CAst in |