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_ops.mli | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'interp/constrexpr_ops.mli') diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index b4f0886ac..1c2348457 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -10,7 +10,6 @@ open Names open Libnames -open Misctypes open Constrexpr (** Constrexpr_ops: utilities on [constr_expr] *) @@ -44,7 +43,7 @@ val local_binders_loc : local_binder_expr list -> Loc.t option val mkIdentC : Id.t -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr -val mkCastC : constr_expr * constr_expr cast_type -> constr_expr +val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr -- cgit v1.2.3