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, 2 insertions, 0 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 9f45187cf..94b7ca96a 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -268,6 +268,8 @@ val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool
val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt
val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, types) Context.Rel.Declaration.pt
+val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
+
(** {5 Unsafe operations} *)
module Unsafe :