From 0489e8b56d7e10f7111c0171960e25d32201b963 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 21:55:33 +0100
Subject: Clenv API using EConstr.

---
 engine/eConstr.ml  | 2 ++
 engine/eConstr.mli | 3 +++
 2 files changed, 5 insertions(+)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 095521e252..7bd708e316 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -560,6 +560,8 @@ let substn_vars n subst c = of_constr (Vars.substn_vars n subst (to_constr c))
 let subst_vars subst c = of_constr (Vars.subst_vars subst (to_constr c))
 let subst_var subst c = of_constr (Vars.subst_var subst (to_constr c))
 
+let subst_univs_level_constr subst c =
+  of_constr (Vars.subst_univs_level_constr subst (to_constr c))
 (** Operations that dot NOT commute with evar-normalization *)
 let noccurn sigma n term =
   let rec occur_rec n c = match kind sigma c with
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 10eb064a3c..e4136a6122 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -171,6 +171,9 @@ val noccur_between : Evd.evar_map -> int -> int -> t -> bool
 
 val closedn : Evd.evar_map -> int -> t -> bool
 val closed0 : Evd.evar_map -> t -> bool
+
+val subst_univs_level_constr : Univ.universe_level_subst -> t -> t
+
 end
 
 (** {5 Unsafe operations} *)
-- 
cgit v1.2.3