From ab6ebfc1f42d96d50763f2dcd6b8322b12613d3d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 6 Oct 2020 14:58:45 +0200
Subject: Further code simplification in arbitrary hint interpretation.

We reuse the standard code path for term interpretation instead of trying
to mangle it.
---
 engine/eConstr.ml  | 3 +++
 engine/eConstr.mli | 1 +
 2 files changed, 4 insertions(+)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index bb2873b486..0c84dee572 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -628,6 +628,9 @@ 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))
 
+let subst_univs_constr subst c =
+  of_constr (UnivSubst.subst_univs_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 a018f4064f..882dfe2848 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -295,6 +295,7 @@ 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
+val subst_univs_constr : Univ.universe_subst -> t -> t
 val subst_of_rel_context_instance : rel_context -> t list -> t list
 
 
-- 
cgit v1.2.3