From 2fd40ff72d3b7b54422b9b00b394c9c446cb5cd7 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 27 Jun 2013 23:04:06 +0000
Subject: Removed the distinction between generic Ltac vars and Let/Intro
 bindings, which permits using only one environment for interning terms.

Ltac semantics was sligthly changed, as it required introducing
a lot of additional coercions from goal variables to other types.
Ltac seemed to be quite non-uniform, as it tried to represent
hypotheses with intropatterns, instead of the dedicated var type.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16612 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/genintern.ml  | 2 +-
 interp/genintern.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/genintern.ml b/interp/genintern.ml
index 00ea3a71bb..12d25c785d 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -13,7 +13,7 @@ open Mod_subst
 open Genarg
 
 type glob_sign = {
-  ltacvars : Id.t list * Id.t list;
+  ltacvars : Id.Set.t;
   ltacrecvars : (Id.t * Nametab.ltac_constant) list;
   gsigma : Evd.evar_map;
   genv : Environ.env }
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 25050fe7c8..9fe553cbaa 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -11,7 +11,7 @@ open Mod_subst
 open Genarg
 
 type glob_sign = {
-  ltacvars : Id.t list * Id.t list;
+  ltacvars : Id.Set.t;
   ltacrecvars : (Id.t * Nametab.ltac_constant) list;
   gsigma : Evd.evar_map;
   genv : Environ.env }
-- 
cgit v1.2.3