Removing subst_defined_metas_evars from Evd.

1 files changed, 13 insertions, 0 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 24e06007e9..123f9b8cd3 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -554,6 +554,19 @@ let isAllowedEvar flags c = match kind_of_term c with
   | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars)
   | _ -> false
 
+
+let subst_defined_metas_evars (bl,el) c =
+  let rec substrec c = match kind_of_term c with
+    | Meta i ->
+      let select (j,_,_) = Int.equal i j in
+      substrec (pi2 (List.find select bl))
+    | Evar (evk,args) ->
+      let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.equal Constr.equal args args' in
+      (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
+
 let check_compatibility env pbty flags (sigma,metasubst,evarsubst) tyM tyN =
   match subst_defined_metas_evars (metasubst,[]) tyM with
   | None -> sigma