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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index f495a81e6..ab595be25 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1461,7 +1461,8 @@ let subst_defined_metas_evars (bl,el) c = substrec (pi2 (List.find select bl)) | Evar (evk,args) -> let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.equal Constr.equal args args' in - substrec (pi3 (List.find select el)) + (try substrec (pi3 (List.find select el)) + with Not_found -> map_constr substrec c) | _ -> map_constr substrec c in try Some (substrec c) with Not_found -> None |