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/pptactic.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/ltac/pptactic.ml')

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