diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-08 17:02:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-08 17:10:45 +0100 |
| commit | c9728f6eba0d4391992e89bdd9886d46fdf16004 (patch) | |
| tree | 5390b97a66479d0cf5000f35fc2aa7636c77e1d5 /proofs/clenvtac.ml | |
| parent | 7750fb5d882b1da4bc2f35c8d28a180c27fbb8a4 (diff) | |
Fixing a bug in change of subst_defined_metas in bcba6d1bc9f769da:
One missing evar was making the whole substitution fail.
The bug actually existed a priori also in the case where only metas
are substituted (i.e. before bcba6d1bc9f769da), leading to limit the
number of situations where it could be effectful.
This fixes current failures of RelationAlgebra and CFGV.
Diffstat (limited to 'proofs/clenvtac.ml')
0 files changed, 0 insertions, 0 deletions