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


From 451acd6ca6a9ce5b86622fb42085eb19e23d6665 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 19 Aug 2019 15:20:31 +0200
Subject: [declare] Use `binding_kind` for implicit kind instead of boolean.

---
 tactics/declare.ml  | 3 +--
 tactics/declare.mli | 2 +-
 2 files changed, 2 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index cdbb3d41d9..17e873f017 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -300,7 +300,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
 (** Declaration of section variables and local definitions *)
 type variable_declaration =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
-  | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
+  | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind }
 
 (* This object is only for things which iterate over objects to find
    variables (only Prettyp.print_context AFAICT) *)
@@ -317,7 +317,6 @@ 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 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
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 89b41076f7..4ae9f6c7ae 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -23,7 +23,7 @@ open Entries
 
 type variable_declaration =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
-  | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
+  | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind }
 
 type 'a constant_entry =
   | DefinitionEntry of 'a Proof_global.proof_entry
-- 
cgit v1.2.3