diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-12-30 16:27:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-12-30 16:52:13 +0100 |
| commit | e80e911ec4fa174ebb4a8e79362dbc7946b49b98 (patch) | |
| tree | b79ca9271993cf2fe12d61741f427e76116bec2e | |
| parent | ea47086be3b724968053525e8fa795b9cdd77800 (diff) | |
Useless Evd.create_evar_defs.
| -rw-r--r-- | toplevel/command.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index bf226b0bf..29a1b3cf2 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 |