From 368a25e4ef14512b00f5799e26c3f615bc540201 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 22 May 2018 00:07:26 +0200
Subject: [api] Misctypes removal: several moves:

- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
---
 plugins/ltac/pptactic.mli | 1 +
 1 file changed, 1 insertion(+)

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

diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 5d2a996183..c14874d6c4 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -19,6 +19,7 @@ open Environ
 open Constrexpr
 open Notation_gram
 open Tacexpr
+open Tactypes
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
-- 
cgit v1.2.3


From 615290d0f9d5cad7c508d45cf4ab89aecff033b2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 1 Jun 2018 02:37:15 +0200
Subject: [api] Remove Misctypes.

We move the last 3 types to more adequate places.
---
 plugins/ltac/pptactic.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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

diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index c14874d6c4..6c09e447a5 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -14,7 +14,6 @@
 open Genarg
 open Geninterp
 open Names
-open Misctypes
 open Environ
 open Constrexpr
 open Notation_gram
@@ -98,7 +97,7 @@ val pr_may_eval :
   ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) ->
   ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t
 
-val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t
+val pr_and_short_name : ('a -> Pp.t) -> 'a Stdarg.and_short_name -> Pp.t
 val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
 
 val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t
-- 
cgit v1.2.3