aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/evd.ml3
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