From 16677f3d4e71b2f971ed36bbbc3b95d8908a1b13 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 17 Dec 2013 15:08:06 +0100
Subject: Removing the need of evarmaps in constr internalization.

Actually, this was wrong, as evars should not appear until interpretation.
Evarmaps were only passed around uselessly, and often fed with dummy or
irrelevant values.
---
 interp/genintern.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'interp/genintern.mli')

diff --git a/interp/genintern.mli b/interp/genintern.mli
index 7027315e7..970f27f66 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -13,7 +13,6 @@ open Genarg
 type glob_sign = {
   ltacvars : Id.Set.t;
   ltacrecvars : Nametab.ltac_constant Id.Map.t;
-  gsigma : Evd.evar_map;
   genv : Environ.env }
 
 (** {5 Internalization functions} *)
-- 
cgit v1.2.3