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.
---
 plugins/ssr/ssrcommon.ml  |  1 -
 plugins/ssr/ssrparser.mlg | 15 +++++++--------
 plugins/ssr/ssrvernac.mlg |  1 -
 3 files changed, 7 insertions(+), 10 deletions(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 33e9f871fd..473612fda7 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -181,7 +181,6 @@ let option_assert_get o msg =
 
 (** Constructors for rawconstr *)
 open Glob_term
-open Decl_kinds
 
 let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)
 
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 175a863ad8..a1f707ffa8 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -32,7 +32,6 @@ open Ppconstr
 
 open Namegen
 open Tactypes
-open Decl_kinds
 open Constrexpr
 open Constrexpr_ops
 
@@ -1337,20 +1336,20 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde
  | [ ssrbvar(bv) ] ->
    { let { CAst.loc=xloc } as x = bvar_lname bv in
      (FwdPose, [BFvar]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) }
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
  | [ "(" ssrbvar(bv) ")" ] ->
    { let { CAst.loc=xloc } as x = bvar_lname bv in
      (FwdPose, [BFvar]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) }
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
  | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] ->
    { let x = bvar_lname bv in
      (FwdPose, [BFdecl 1]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Explicit, t)], mkCHole (Some loc)) }
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
  | [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] ->
    { let xs = List.map bvar_lname (bv :: bvs) in
      let n = List.length xs in
      (FwdPose, [BFdecl n]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Explicit, t)], mkCHole (Some loc)) }
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
  | [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] ->
    { (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) }
  | [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] ->
@@ -1362,7 +1361,7 @@ GRAMMAR EXTEND Gram
   ssrbinder: [
   [  ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> {
      (FwdPose, [BFvar]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) } ]
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ]
   ];
 END
 
@@ -1391,7 +1390,7 @@ let push_binders c2 bs =
 
 let rec fix_binders = let open CAst in function
   | (_, { v = CLambdaN ([CLocalAssum(xs, _, t)], _) } ) :: bs ->
-      CLocalAssum (xs, Default Explicit, t) :: fix_binders bs
+      CLocalAssum (xs, Default Glob_term.Explicit, t) :: fix_binders bs
   | (_, { v = CLetIn (x, v, oty, _) } ) :: bs ->
     CLocalDef (x, v, oty) :: fix_binders bs
   | _ -> []
@@ -1521,7 +1520,7 @@ let intro_id_to_binder = List.map (function
   | IPatId id ->
       let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in
       (FwdPose, [BFvar]),
-        CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)],
+        CAst.make @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, mkCHole xloc)],
           mkCHole None)
   | _ -> anomaly "non-id accepted as binder")
 
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 0adabb0673..f3f1d713e9 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -27,7 +27,6 @@ open Notation_ops
 open Notation_term
 open Glob_term
 open Stdarg
-open Decl_kinds
 open Pp
 open Ppconstr
 open Printer
-- 
cgit v1.2.3