aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/eConstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/eConstr.mli')
-rw-r--r--engine/eConstr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 913825a9f..ecb36615f 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -321,7 +321,7 @@ sig
val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
(** Physical identity. Does not care for defined evars. *)
- val to_named_context : (t, types) Context.Named.pt -> Context.Named.t
+ val to_named_context : (t, types) Context.Named.pt -> Constr.named_context
val to_sorts : ESorts.t -> Sorts.t
(** Physical identity. Does not care for normalization. *)