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