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 /parsing/g_constr.mlg | |
| 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 'parsing/g_constr.mlg')
| -rw-r--r-- | parsing/g_constr.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 4a9190c10a..6df97609f5 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -500,9 +500,9 @@ GRAMMAR EXTEND Gram | "{"; id=name; idl=LIST1 name; "}" -> { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> - { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc } + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Explicit, b), t)) tc } | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> - { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc } + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, b), t)) tc } | "'"; p = pattern LEVEL "0" -> { let (p, ty) = match p.CAst.v with |