From 58630ad9a0b94a804a39a3d99f982965292692c7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 21 May 2018 23:54:55 +0200
Subject: [api] Misctypes removal: miscellaneous aliases.

---
 plugins/ltac/g_tactic.ml4     | 9 +++++----
 plugins/ltac/pltac.mli        | 6 +++---
 plugins/ltac/tactic_debug.mli | 2 +-
 3 files changed, 9 insertions(+), 8 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 15db4ca6a..038d55e4b 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -11,6 +11,7 @@
 open Pp
 open CErrors
 open Util
+open Names
 open Tacexpr
 open Genredexpr
 open Constrexpr
@@ -383,19 +384,19 @@ GEXTEND Gram
   ;
   hypident:
     [ [ id = id_or_meta ->
-        let id : Misctypes.lident = id in
+        let id : lident = id in
         id,InHyp
       | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" ->
-        let id : Misctypes.lident = id in
+        let id : lident = id in
         id,InHypTypeOnly
       | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" ->
-        let id : Misctypes.lident = id in
+        let id : lident = id in
         id,InHypValueOnly
     ] ]
   ;
   hypident_occ:
     [ [ (id,l)=hypident; occs=occs ->
-        let id : Misctypes.lident = id in
+        let id : lident = id in
         ((occs,id),l) ] ]
   ;
   in_clause:
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 434feba95..de23d2f8e 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -20,7 +20,7 @@ open Misctypes
 val open_constr : constr_expr Gram.entry
 val constr_with_bindings : constr_expr with_bindings Gram.entry
 val bindings : constr_expr bindings Gram.entry
-val hypident : (lident * Locus.hyp_location_flag) Gram.entry
+val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry
 val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
 val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
 val uconstr : constr_expr Gram.entry
@@ -29,8 +29,8 @@ val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.ent
 val int_or_var : int or_var Gram.entry
 val simple_tactic : raw_tactic_expr Gram.entry
 val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry
-val in_clause : lident Locus.clause_expr Gram.entry
-val clause_dft_concl : lident Locus.clause_expr Gram.entry
+val in_clause : Names.lident Locus.clause_expr Gram.entry
+val clause_dft_concl : Names.lident Locus.clause_expr Gram.entry
 val tactic_arg : raw_tactic_arg Gram.entry
 val tactic_expr : raw_tactic_expr Gram.entry
 val binder_tactic : raw_tactic_expr Gram.entry
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 734e76b56..175341df0 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -76,7 +76,7 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
 
 (** Prints a logic failure message for a rule *)
 val db_breakpoint : debug_info ->
-  Misctypes.lident message_token list -> unit Proofview.NonLogical.t
+  lident message_token list -> unit Proofview.NonLogical.t
 
 val extract_ltac_trace :
   ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located
-- 
cgit v1.2.3