aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/eConstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/eConstr.ml')
-rw-r--r--engine/eConstr.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index b6b202cd9..f50a8b850 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -634,6 +634,9 @@ let closedn sigma n c =
let closed0 sigma c = closedn sigma 0 c
+let subst_of_rel_context_instance ctx subst =
+ List.map of_constr (Vars.subst_of_rel_context_instance (List.map unsafe_to_rel_decl ctx) (List.map to_constr subst))
+
end
let rec isArity sigma c =