From 64041ca0c17430085c20b7754277313fdb439a6a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 26 Aug 2014 00:12:09 +0200
Subject: Fix compilation error due to commented code in previous commit by
 Hugo.

---
 pretyping/unification.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 34fac5e75f..5f7e2916b4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1193,8 +1193,8 @@ let indirect_dependency d decls =
   pi1 (List.hd (List.filter (fun (id,_,_) -> dependent_in_decl (mkVar id) d) decls))
 
 let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env initial_sigma (sigma,c) =
-(*  let sigma = Pretyping.solve_remaining_evars flags env initial_sigma sigma
-in*) Evd.evar_universe_context sigma, nf_evar sigma c
+  let sigma = Pretyping.solve_remaining_evars flags env initial_sigma sigma
+  in Evd.evar_universe_context sigma, nf_evar sigma c
 
 let default_matching_flags sigma = {
   modulo_conv_on_closed_terms = Some empty_transparent_state;
-- 
cgit v1.2.3