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. --- library/decl_kinds.ml | 11 ----------- 1 file changed, 11 deletions(-) delete mode 100644 library/decl_kinds.ml (limited to 'library/decl_kinds.ml') diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml deleted file mode 100644 index 17746645ee..0000000000 --- a/library/decl_kinds.ml +++ /dev/null @@ -1,11 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(*