From e80e911ec4fa174ebb4a8e79362dbc7946b49b98 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 30 Dec 2013 16:27:28 +0100
Subject: Useless Evd.create_evar_defs.

---
 toplevel/command.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index bf226b0bf9..29a1b3cf2d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -620,8 +620,7 @@ let nf_evar_context sigma ctx =
 
 let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
-  let sigma = Evd.empty in
-  let evdref = ref (Evd.create_evar_defs sigma) in
+  let evdref = ref Evd.empty in
   let env = Global.env() in
   let _, ((env', binders_rel), impls) = interp_context_evars evdref env bl in
   let len = List.length binders_rel in
-- 
cgit v1.2.3