From d7e7e9a62fd951b2103d2b6fb9ce2589a16022ca Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Nov 2014 17:52:35 +0100
Subject: Universes.nf_evars_and_universes_opt_subst substitutes evars eagerly.

This is a continuation of the previous patch.
---
 library/universes.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/library/universes.ml b/library/universes.ml
index 708324aede..438e6cc532 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -547,8 +547,9 @@ let nf_evars_and_universes_opt_subst f subst =
   let lsubst = Univ.level_subst_of subst in
   let rec aux c =
     match kind_of_term c with
-    | Evar (evdk, _ as ev) ->
-      (match try f ev with Not_found -> None with
+    | Evar (evk, args) ->
+      let args = Array.map aux args in
+      (match try f (evk, args) with Not_found -> None with
       | None -> c
       | Some c -> aux c)
     | Const pu -> 
-- 
cgit v1.2.3