[api] Misctypes removal: several moves:

- move_location to proofs/logic.
- intro_pattern_naming to Namegen.

6 files changed, 36 insertions, 21 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 450fcddfd..79b7e1599 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -26,7 +26,7 @@ open Tacred
 open Pretype_errors
 open Evarutil
 open Unification
-open Misctypes
+open Tactypes
 
 (******************************************************************)
 (* Clausal environments *)
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index b85c4fc51..f9506290a 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -18,7 +18,7 @@ open Environ
 open Evd
 open EConstr
 open Unification
-open Misctypes
+open Tactypes
 
 (** {6 The Type of Constructions clausale environments.} *)
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 95c30d815..e8ca71993 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -23,7 +23,6 @@ open Typing
 open Proof_type
 open Type_errors
 open Retyping
-open Misctypes
 
 module NamedDecl = Context.Named.Declaration
 
@@ -185,6 +184,22 @@ let check_decl_position env sigma sign d =
  * on the right side [right] if [toleft=false].
  * If [with_dep] then dependent hypotheses are moved accordingly. *)
 
+(** Move destination for hypothesis *)
+
+type 'id move_location =
+  | MoveAfter of 'id
+  | MoveBefore of 'id
+  | MoveFirst
+  | MoveLast (** can be seen as "no move" when doing intro *)
+
+(** Printing of [move_location] *)
+
+let pr_move_location pr_id = function
+  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
+  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
+  | MoveFirst -> str " at top"
+  | MoveLast -> str " at bottom"
+
 let move_location_eq m1 m2 = match m1, m2 with
 | MoveAfter id1, MoveAfter id2 -> Id.equal id1 id2
 | MoveBefore id1, MoveBefore id2 -> Id.equal id1 id2
@@ -236,7 +251,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
 	      (first, d::middle)
             else
 	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
-	        Miscprint.pr_move_location Id.print hto ++
+                pr_move_location Id.print hto ++
 	        str (if toleft then ": it occurs in the type of " else ": it depends on ")
 	        ++ Id.print hyp ++ str ".")
           else
diff --git a/proofs/logic.mli b/proofs/logic.mli
index dc471bb5f..9db54732b 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -58,12 +58,23 @@ val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a
 
 val catchable_exception : exn -> bool
 
+(** Move destination for hypothesis *)
+
+type 'id move_location =
+  | MoveAfter of 'id
+  | MoveBefore of 'id
+  | MoveFirst
+  | MoveLast (** can be seen as "no move" when doing intro *)
+
+val pr_move_location :
+  ('a -> Pp.t) -> 'a move_location -> Pp.t
+
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
   EConstr.named_declaration -> Environ.named_context_val
 
-val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t Misctypes.move_location ->
+val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location ->
   Environ.named_context_val -> Environ.named_context_val
 
 val insert_decl_in_named_context : Evd.evar_map ->
-  EConstr.named_declaration -> Id.t Misctypes.move_location ->
+  EConstr.named_declaration -> Id.t move_location ->
   Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml
index 1a63ff673..ec17b8076 100644
--- a/proofs/miscprint.ml
+++ b/proofs/miscprint.ml
@@ -10,7 +10,7 @@
 
 open Pp
 open Names
-open Misctypes
+open Tactypes
 
 (** Printing of [intro_pattern] *)
 
@@ -20,7 +20,7 @@ let rec pr_intro_pattern prc {CAst.v=pat} = match pat with
   | IntroNaming p -> pr_intro_pattern_naming p
   | IntroAction p -> pr_intro_pattern_action prc p
 
-and pr_intro_pattern_naming = function
+and pr_intro_pattern_naming = let open Namegen in function
   | IntroIdentifier id -> Id.print id
   | IntroFresh id -> str "?" ++ Id.print id
   | IntroAnonymous -> str "?"
@@ -43,14 +43,6 @@ and pr_or_and_intro_pattern prc = function
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll)
       ++ str "]"
 
-(** Printing of [move_location] *)
-
-let pr_move_location pr_id = function
-  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
-  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
-  | MoveFirst -> str " at top"
-  | MoveLast -> str " at bottom"
-
 (** Printing of bindings *)
 let pr_binding prc = let open CAst in function
   | {loc;v=(NamedHyp id, c)} -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c)
diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli
index 79790a277..f4e2e683d 100644
--- a/proofs/miscprint.mli
+++ b/proofs/miscprint.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Misctypes
+open Tactypes
 
 (** Printing of [intro_pattern] *)
 
@@ -18,13 +18,10 @@ val pr_intro_pattern :
 val pr_or_and_intro_pattern :
   ('a -> Pp.t) -> 'a or_and_intro_pattern_expr -> Pp.t
 
-val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.t
+val pr_intro_pattern_naming : Namegen.intro_pattern_naming_expr -> Pp.t
 
 (** Printing of [move_location] *)
 
-val pr_move_location :
-  ('a -> Pp.t) -> 'a move_location -> Pp.t
-
 val pr_bindings :
   ('a -> Pp.t) ->
   ('a -> Pp.t) -> 'a bindings -> Pp.t