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

---
 interp/constrexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/constrexpr.ml')

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index ca6ea94f09..d6b395e01c 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -95,7 +95,7 @@ and constr_expr_r =
   | CIf of constr_expr * (lname option * constr_expr option)
          * constr_expr * constr_expr
   | CHole   of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
-  | CPatVar of patvar
+  | CPatVar of Pattern.patvar
   | CEvar   of Glob_term.existential_name * (Id.t * constr_expr) list
   | CSort   of Glob_term.glob_sort
   | CCast   of constr_expr * constr_expr cast_type
-- 
cgit v1.2.3


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.
---
 interp/constrexpr.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'interp/constrexpr.ml')

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index d6b395e01c..60f2c683a0 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -10,7 +10,6 @@
 
 open Names
 open Libnames
-open Misctypes
 open Decl_kinds
 
 (** {6 Concrete syntax for terms } *)
@@ -94,11 +93,11 @@ and constr_expr_r =
                  constr_expr * constr_expr
   | CIf of constr_expr * (lname option * constr_expr option)
          * constr_expr * constr_expr
-  | CHole   of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
+  | CHole   of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
   | CPatVar of Pattern.patvar
   | CEvar   of Glob_term.existential_name * (Id.t * constr_expr) list
   | CSort   of Glob_term.glob_sort
-  | CCast   of constr_expr * constr_expr cast_type
+  | CCast   of constr_expr * constr_expr Glob_term.cast_type
   | CNotation of notation * constr_notation_substitution
   | CGeneralization of binding_kind * abstraction_kind option * constr_expr
   | CPrim of prim_token
-- 
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.
---
 interp/constrexpr.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'interp/constrexpr.ml')

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 60f2c683a0..d725f5afaf 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -22,6 +22,15 @@ type name_decl = lname * universe_decl_expr option
 
 type notation = string
 
+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. *)
+
 type explicitation =
   | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
   | ExplByName of Id.t
-- 
cgit v1.2.3