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 /printing/ppconstr.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 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 78733784a7..9d3ed40f6c 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -339,8 +339,7 @@ let tag_var = tag Tag.variable let pr_binder many pr (nal,k,t) = match k with - | Generalized (b, b', t') -> - assert (match b with Implicit -> true | _ -> false); + | Generalized (b', t') -> begin match nal with |[{loc; v=Anonymous}] -> hov 1 (str"`" ++ (surround_impl b' |