From 62d5ef53da153394c69b52cc707b72d53eaeac44 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 4 Aug 2016 15:32:48 +0200
Subject: Simplifying code in evar generation.

We remove in particular a dubious use of an environment in fresh name
generation. The code was using the wrong environment in a function only
depending on the rel context which was resetted most of the time. This
might change the generated names in extremely rare occurences.
---
 engine/evarutil.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/evarutil.mli')

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index a4200d762b..95b8b3e0bb 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -202,9 +202,9 @@ val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> ty
 val push_rel_decl_to_named_context :
   Context.Rel.Declaration.t ->
   Vars.substl * (Names.Id.t * Constr.constr) list *
-  Names.Id.t list * Environ.env ->
+  Names.Id.t list * Context.Named.t ->
   Term.constr list * (Names.Id.t * Constr.constr) list *
-  Names.Id.t list * Environ.env
+  Names.Id.t list * Context.Named.t
 
 val push_rel_context_to_named_context : Environ.env -> types ->
   named_context_val * types * constr list * constr list * (identifier*constr) list
-- 
cgit v1.2.3