From 21269d0fef6794a672c36abdc5760889adc0e09c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 16 May 2019 14:21:37 +0200
Subject: 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.
---
 printing/ppconstr.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'printing')

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'
-- 
cgit v1.2.3