From 08fdf3c7361c75037e12c5cd0e9f965165fed498 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 4 Jan 2016 21:19:50 +0100
Subject: fixup d2b468a, evar normalization is needed

---
 stm/stm.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/stm/stm.ml b/stm/stm.ml
index 3d007004e2..168d8bf084 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1488,6 +1488,7 @@ end = struct (* {{{ *)
         match Evd.(evar_body (find sigma r_goal)) with
         | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress")
         | Evd.Evar_defined t ->
+            let t = Evarutil.nf_evar sigma t in
             if Evarutil.is_ground_term sigma t then
               t, Evd.evar_universe_context sigma
             else Errors.errorlabstrm "Stm" (str"The solution is not ground")
-- 
cgit v1.2.3