From a74e055acf48583c6fece5d22c805736679376b2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 18 Aug 2019 20:27:52 +0200
Subject: [api] Move handling of variable implicit data to impargs

We move `binder_kind` to the pretyping AST, removing the last data
type in the now orphaned file `Decl_kinds`.

This seems a better fit, as this data is not relevant to the lower
layers but only used in `Impargs`.

We also move state keeping to `Impargs`, so now implicit declaration
must include the type. We also remove a duplicated function.
---
 vernac/classes.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'vernac/classes.ml')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 075d89d0df..d5f5656e1d 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -28,9 +28,7 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 (*i*)
 
-open Decl_kinds
-
-let set_typeclass_transparency c local b = 
+let set_typeclass_transparency c local b =
   Hints.add_hints ~local [typeclasses_db]
     (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b))
 
@@ -527,7 +525,7 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri
 let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
   let tclass =
-    if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass)
+    if generalize then CAst.make @@ CGeneralization (Glob_term.Implicit, Some AbsPi, tclass)
     else tclass
   in
   let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in
-- 
cgit v1.2.3