aboutsummaryrefslogtreecommitdiff
path: root/kernel/vmvalues.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vmvalues.mli')
-rw-r--r--kernel/vmvalues.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index 08d05a038c..6eedcf1d37 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -81,7 +81,7 @@ type zipper =
| Zapp of arguments
| Zfix of vfix * arguments (** might be empty *)
| Zswitch of vswitch
- | Zproj of Constant.t (* name of the projection *)
+ | Zproj of Projection.Repr.t (* name of the projection *)
type stack = zipper list
@@ -108,11 +108,11 @@ val val_of_rel : int -> values
val val_of_named : Id.t -> values
val val_of_constant : Constant.t -> values
val val_of_evar : Evar.t -> values
-val val_of_proj : Constant.t -> values -> values
+val val_of_proj : Projection.Repr.t -> values -> values
val val_of_atom : atom -> values
external val_of_annot_switch : annot_switch -> values = "%identity"
-external val_of_proj_name : Constant.t -> values = "%identity"
+external val_of_proj_name : Projection.Repr.t -> values = "%identity"
(** Destructors *)