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.
---
 tactics/declare.ml   | 8 ++++----
 tactics/hipattern.ml | 1 -
 2 files changed, 4 insertions(+), 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index e093a27728..cdbb3d41d9 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -317,7 +317,7 @@ let declare_variable ~name ~kind d =
     | SectionLocalAssum {typ;univs;poly;impl} ->
       let () = declare_universe_context ~poly univs in
       let () = Global.push_named_assum (name,typ) in
-      let impl = if impl then Decl_kinds.Implicit else Decl_kinds.Explicit in
+      let impl = if impl then Glob_term.Implicit else Glob_term.Explicit in
       impl, true, poly
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
@@ -342,14 +342,14 @@ let declare_variable ~name ~kind d =
         secdef_type = de.proof_entry_type;
       } in
       let () = Global.push_named_def (name, se) in
-      Decl_kinds.Explicit, de.proof_entry_opaque,
+      Glob_term.Explicit, de.proof_entry_opaque,
       poly
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
-  add_section_variable ~name ~kind:impl ~poly;
+  add_section_variable ~name ~poly;
   Decls.(add_variable_data name {opaque;kind});
   add_anonymous_leaf (inVariable ());
-  Impargs.declare_var_implicits name;
+  Impargs.declare_var_implicits ~impl name;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
 
 (** Declaration of inductive blocks *)
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index a3a88df21e..61e0e41eb9 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -258,7 +258,6 @@ type equation_kind =
 exception NoEquationFound
 
 open Glob_term
-open Decl_kinds
 open Evar_kinds
 
 let mkPattern c = snd (Patternops.pattern_of_glob_constr c)
-- 
cgit v1.2.3