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/ltac/g_tactic.mlg | 5 ++---
 plugins/ltac/pptactic.ml  | 3 +--
 2 files changed, 3 insertions(+), 5 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 7cd43cb5cd..9b52b710c1 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -24,7 +24,6 @@ open Tactypes
 open Tactics
 open Inv
 open Locus
-open Decl_kinds
 
 open Pcoq
 
@@ -450,9 +449,9 @@ GRAMMAR EXTEND Gram
       | -> { true } ] ]
   ;
   simple_binder:
-    [ [ na=name -> { ([na],Default Explicit, CAst.make ~loc @@
+    [ [ na=name -> { ([na],Default Glob_term.Explicit, CAst.make ~loc @@
                     CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) }
-      | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Explicit,c) }
+      | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Glob_term.Explicit,c) }
     ] ]
   ;
   fixdecl:
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 0e38ce575b..6df068883c 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -20,7 +20,6 @@ open Stdarg
 open Notation_gram
 open Tactypes
 open Locus
-open Decl_kinds
 open Genredexpr
 open Ppconstr
 open Pputils
@@ -1097,7 +1096,7 @@ let pr_goal_selector ~toplevel s =
     let rec strip_ty acc n ty =
       if Int.equal n 0 then (List.rev acc, (ty,None)) else
         match DAst.get ty with
-            Glob_term.GProd(na,Explicit,a,b) ->
+            Glob_term.GProd(na,Glob_term.Explicit,a,b) ->
               strip_ty (([CAst.make na],(a,None))::acc) (n-1) b
           | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
-- 
cgit v1.2.3