From 31e686c2904c3015eaec18ce502d4e8afe565850 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Aug 2017 18:17:19 +0200
Subject: Rolling our own dynamic types for Ltac2.

This prevents careless confusions with generic arguments from Coq.
---
 src/tac2expr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/tac2expr.mli')

diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 42203a32e5..0b02ba2656 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -185,7 +185,7 @@ type valexpr =
   (** Closures *)
 | ValOpn of KerName.t * valexpr array
   (** Open constructors *)
-| ValExt : 'a Geninterp.Val.typ * 'a -> valexpr
+| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
   (** Arbitrary data *)
 
 and closure = {
-- 
cgit v1.2.3