From ca14b0bb67c9db000736333a056fc147c6f5199c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 27 Sep 2015 14:16:54 +0200
Subject: Removing uselessly duplicated function in Evd.

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index ec0e1d2f4e..a10d8a0747 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1095,7 +1095,7 @@ let minimal_free_rels_rec env sigma =
 
 let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
   let sigdata = find_sigma_data env sort_of_ty in
-  let evdref = ref (Evd.create_goal_evar_defs sigma) in
+  let evdref = ref (Evd.clear_metas sigma) in
   let rec sigrec_clausal_form siglen p_i =
     if Int.equal siglen 0 then
       (* is the default value typable with the expected type *)
-- 
cgit v1.2.3