aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrexpr_ops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrexpr_ops.mli')
-rw-r--r--interp/constrexpr_ops.mli7
1 files changed, 3 insertions, 4 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index b4f0886ac..46aef1c78 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] *)
@@ -42,9 +41,9 @@ val local_binders_loc : local_binder_expr list -> Loc.t option
(** {6 Constructors}*)
val mkIdentC : Id.t -> constr_expr
-val mkRefC : reference -> constr_expr
+val mkRefC : qualid -> 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
@@ -62,7 +61,7 @@ val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -
(** {6 Destructors}*)
-val coerce_reference_to_id : reference -> Id.t
+val coerce_reference_to_id : qualid -> Id.t
(** FIXME: nothing to do here *)
val coerce_to_id : constr_expr -> lident