diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-04 15:32:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-04 19:15:59 +0200 |
| commit | 62d5ef53da153394c69b52cc707b72d53eaeac44 (patch) | |
| tree | 7f9062fe21d0a275cc7989ab49dd81fb81b68774 /engine/evarutil.mli | |
| parent | b283c7674c4bff8ac2be52e896a40ba155c3d994 (diff) | |
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.
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index a4200d762..95b8b3e0b 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 |