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 +++
 1 file changed, 3 insertions(+)

(limited to 'engine/eConstr.ml')

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
-- 
cgit v1.2.3