diff options
Diffstat (limited to 'engine/eConstr.ml')
-rw-r--r-- | engine/eConstr.ml | 3 |
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 = |