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.
---
 interp/constrexpr.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/constrexpr.ml')

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 9f778d99e9..3ebbbdfb88 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -40,8 +40,8 @@ type explicitation =
 
 type binder_kind =
   | Default of binding_kind
-  | Generalized of binding_kind * binding_kind * bool
-      (** Inner binding, outer bindings, typeclass-specific flag
+  | Generalized of binding_kind * bool
+      (** (Inner binding always Implicit) Outer bindings, typeclass-specific flag
 	 for implicit generalization of superclasses *)
 
 type abstraction_kind = AbsLambda | AbsPi
-- 
cgit v1.2.3