From 9cadb903b7c3a3be8014152b293cd5ade3a7c8b7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 27 Sep 2015 16:36:10 +0200
Subject: Removing subst_defined_metas_evars from Evd.

---
 pretyping/unification.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'pretyping')

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
-- 
cgit v1.2.3