From 72ac4b32ac26fdba751ae48568d28b4dbb8edd14 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 15 Sep 2016 18:11:54 +0200
Subject: Untangling Tacexpr from lower strata.

---
 interp/genintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/genintern.ml')

diff --git a/interp/genintern.ml b/interp/genintern.ml
index 693101a476..be7abfa995 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -16,7 +16,7 @@ type glob_sign = {
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
 type 'glb subst_fun = substitution -> 'glb -> 'glb
-type 'glb ntn_subst_fun = Tacexpr.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
 
 module InternObj =
 struct
-- 
cgit v1.2.3