From 3227a799ff592ce7e474c84b96df00aa4ed38055 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 25 Jun 2013 16:28:13 +0000
Subject: Useless use of maps in constr internalizing.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16607 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/constrintern.mli')

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 32e878165..2a8085682 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -68,7 +68,7 @@ val compute_internalization_env : env -> var_internalization_type ->
   Id.t list -> types list -> Impargs.manual_explicitation list list ->
   internalization_env
 
-type ltac_sign = Id.t list * unbound_ltac_var_map
+type ltac_sign = Id.t list * Id.Set.t
 
 type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
 
-- 
cgit v1.2.3