[api] Misctypes removal: several moves:

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

10 files changed, 86 insertions, 102 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1edce17bd..aa1c23f52 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2103,7 +2103,7 @@ let mk_JMeq_refl evdref typ x =
 
 let hole na = DAst.make @@
   GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na),
-         Misctypes.IntroAnonymous, None)
+         IntroAnonymous, None)
 
 let constr_of_pat env evdref arsign pat avoid =
   let rec typ env (ty, realargs) pat avoid =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index e6cfe1f76..df89d9eac 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -27,7 +27,6 @@ open Libnames
 open Globnames
 open Nametab
 open Mod_subst
-open Misctypes
 open Decl_kinds
 open Context.Named.Declaration
 open Ltac_pretype
@@ -1027,7 +1026,7 @@ let rec subst_glob_constr subst = DAst.map (function
 
   | GCast (r1,k) as raw ->
       let r1' = subst_glob_constr subst r1 in
-      let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in
+      let k' = smartmap_cast_type (subst_glob_constr subst) k in
       if r1' == r1 && k' == k then raw else GCast (r1',k')
 
   | GProj (p,c) as raw ->
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 63618c918..71a457280 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -11,10 +11,8 @@
 open Util
 open CAst
 open Names
-open Constr
 open Nameops
 open Globnames
-open Misctypes
 open Glob_term
 open Evar_kinds
 open Ltac_pretype
@@ -48,12 +46,20 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
   let comp2 = f ty in
   (na,k,comp1,comp2)
 
+
+let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
+| GProp, GProp -> true
+| GSet, GSet -> true
+| GType l1, GType l2 ->
+   List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2
+| _ -> false
+
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
   | Decl_kinds.Explicit, Decl_kinds.Explicit -> true
   | Decl_kinds.Implicit, Decl_kinds.Implicit -> true
   | (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false
 
-let case_style_eq s1 s2 = match s1, s2 with
+let case_style_eq s1 s2 = let open Constr in match s1, s2 with
   | LetStyle, LetStyle -> true
   | IfStyle, IfStyle -> true
   | LetPatternStyle, LetPatternStyle -> true
@@ -141,10 +147,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
     fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 &&
     Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 &&
     Array.equal f c1 c2 && Array.equal f t1 t2
-  | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2
+  | GSort s1, GSort s2 -> glob_sort_eq s1 s2
   | GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) ->
     Option.equal (==) gn1 gn2 (** Only thing sensible *) &&
-    Miscops.intro_pattern_naming_eq nam1 nam2
+    Namegen.intro_pattern_naming_eq nam1 nam2
   | GCast (c1, t1), GCast (c2, t2) ->
     f c1 c2 && cast_type_eq f t1 t2
   | GProj (p1, t1), GProj (p2, t2) ->
@@ -154,6 +160,21 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
 
 let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
 
+(** Mapping [cast_type] *)
+
+let map_cast_type f = function
+  | CastConv a -> CastConv (f a)
+  | CastVM a -> CastVM (f a)
+  | CastCoerce -> CastCoerce
+  | CastNative a -> CastNative (f a)
+
+let smartmap_cast_type f c =
+  match c with
+    | CastConv a -> let a' = f a in if a' == a then c else CastConv a'
+    | CastVM a -> let a' = f a in if a' == a then c else CastVM a'
+    | CastCoerce -> CastCoerce
+    | CastNative a -> let a' = f a in if a' == a then c else CastNative a'
+
 let map_glob_constr_left_to_right f = DAst.map (function
   | GApp (g,args) ->
       let comp1 = f g in
@@ -194,7 +215,7 @@ let map_glob_constr_left_to_right f = DAst.map (function
       GRec (fk,idl,comp1,comp2,comp3)
   | GCast (c,k) ->
       let comp1 = f c in
-      let comp2 = Miscops.map_cast_type f k in
+      let comp2 = map_cast_type f k in
       GCast (comp1,comp2)
   | GProj (p,c) ->
     GProj (p, f c)
@@ -539,7 +560,7 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo
   | PatVar (Name id) when not isclosed ->
       GVar id
   | PatVar Anonymous when not isclosed ->
-      GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Misctypes.IntroAnonymous,None)
+      GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Namegen.IntroAnonymous,None)
   | _ -> raise Not_found
   ) x
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 124440f5d..c967f4e88 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -13,6 +13,8 @@ open Glob_term
 
 (** Equalities *)
 
+val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
+
 val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
 
 val alias_of_pat : 'a cases_pattern_g -> Name.t
@@ -20,10 +22,15 @@ val alias_of_pat : 'a cases_pattern_g -> Name.t
 val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g
 
 val cast_type_eq : ('a -> 'a -> bool) ->
-  'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
+  'a cast_type -> 'a cast_type -> bool
 
 val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool
 
+(** Mapping [cast_type] *)
+
+val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
+val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
+
 (** Operations on [glob_constr] *)
 
 val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 6ecb479e6..54fa5328f 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -18,7 +18,6 @@
 
 open Names
 open Decl_kinds
-open Misctypes
 
 type existential_name = Id.t
 
@@ -41,6 +40,14 @@ type glob_constraint = glob_level * Univ.constraint_type * glob_level
 type sort_info = (Libnames.reference * int) option list
 type glob_sort = sort_info glob_sort_gen
 
+(** Casts *)
+
+type 'a cast_type =
+  | CastConv of 'a
+  | CastVM of 'a
+  | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
+  | CastNative of 'a
+
 (**  The kind of patterns that occurs in "match ... with ... end"
 
      locs here refers to the ident's location, not whole pat *)
@@ -73,7 +80,7 @@ type 'a glob_constr_r =
   | GRec  of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array *
              'a glob_constr_g array * 'a glob_constr_g array
   | GSort of glob_sort
-  | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option
+  | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
   | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type
   | GProj of Projection.t * 'a glob_constr_g
 and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
deleted file mode 100644
index 1697e54ab..000000000
--- a/pretyping/miscops.ml
+++ /dev/null
@@ -1,55 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Util
-open Misctypes
-
-(** Mapping [cast_type] *)
-
-let map_cast_type f = function
-  | CastConv a -> CastConv (f a)
-  | CastVM a -> CastVM (f a)
-  | CastCoerce -> CastCoerce
-  | CastNative a -> CastNative (f a)
-
-let smartmap_cast_type f c =
-  match c with
-    | CastConv a -> let a' = f a in if a' == a then c else CastConv a'
-    | CastVM a -> let a' = f a in if a' == a then c else CastVM a'
-    | CastCoerce -> CastCoerce
-    | CastNative a -> let a' = f a in if a' == a then c else CastNative a'
-
-(** Equalities on [glob_sort] *)
-
-let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
-| GProp, GProp -> true
-| GSet, GSet -> true
-| GType l1, GType l2 ->
-   List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2
-| _ -> false
-
-let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
-| IntroAnonymous, IntroAnonymous -> true
-| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2
-| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
-| _ -> false
-
-(** Mapping bindings *)
-
-let map_explicit_bindings f l =
-  let map = CAst.map (fun (hyp, x) -> (hyp, f x)) in
-  List.map map l
-
-let map_bindings f = function
-| ImplicitBindings l -> ImplicitBindings (List.map f l)
-| ExplicitBindings expl -> ExplicitBindings (map_explicit_bindings f expl)
-| NoBindings -> NoBindings
-
-let map_with_bindings f (x, bl) = (f x, map_bindings f bl)
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
deleted file mode 100644
index 6a84fb9eb..000000000
--- a/pretyping/miscops.mli
+++ /dev/null
@@ -1,30 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Misctypes
-
-(** Mapping [cast_type] *)
-
-val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
-val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
-
-(** Equalities on [glob_sort] *)
-
-val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
-
-(** Equalities on [intro_pattern_naming] *)
-
-val intro_pattern_naming_eq :
-  intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool
-
-(** Mapping bindings *)
-
-val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings
-val map_with_bindings : ('a -> 'b) -> 'a with_bindings -> 'b with_bindings
diff --git a/pretyping/misctypes.ml b/pretyping/misctypes.ml
new file mode 100644
index 000000000..c66c9b1b8
--- /dev/null
+++ b/pretyping/misctypes.ml
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+(** Some utility types for parsing *)
+
+type 'a or_var =
+  | ArgArg of 'a
+  | ArgVar of lident
+
+type 'a and_short_name = 'a * lident option
+
+type 'a or_by_notation_r =
+  | AN of 'a
+  | ByNotation of (string * string option)
+
+type 'a or_by_notation = 'a or_by_notation_r CAst.t
+
+(* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
+   but this formulation avoids a useless dependency. *)
+
+(** Various flags *)
+
+type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
+type evars_flag = bool     (* true = pose evars       false = fail on evars *)
+type rec_flag = bool       (* true = recursive        false = not recursive *)
+type advanced_flag = bool  (* true = advanced         false = basic *)
+type letin_flag = bool     (* true = use local def    false = use Leibniz *)
+type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 9342b4cc7..622a8e982 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -18,7 +18,6 @@ open Constr
 open Glob_term
 open Pp
 open Mod_subst
-open Misctypes
 open Decl_kinds
 open Pattern
 open Environ
@@ -47,7 +46,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) ->
   Name.equal v1 v2 && constr_pattern_eq b1 b2 &&
   Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2
-| PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2
+| PSort s1, PSort s2 -> Glob_ops.glob_sort_eq s1 s2
 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2
 | PIf (t1, l1, r1), PIf (t2, l2, r2) ->
   constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2
@@ -418,7 +417,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (nal,(_,None),b,c) ->
       let mkGLambda na c = DAst.make ?loc @@
-	GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in
+        GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None),c) in
       let c = List.fold_right mkGLambda nal c in
       let cip =
 	{ cip_style = LetStyle;
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b2507b5f2..9e024b1c2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -45,7 +45,6 @@ open Pretype_errors
 open Glob_term
 open Glob_ops
 open Evarconv
-open Misctypes
 open Ltac_pretype
 
 module NamedDecl = Context.Named.Declaration