From 446b9c571c29f740475e39c19c4037b8102f1f21 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 4 Dec 2014 09:17:47 +0100
Subject: Some refactoring following previous commit.

Just hoisted a definition out of a loop. Not that this part of the code is time critical at all. I just feel it's cleaner.---
 proofs/proofview.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 827fe56a6d..7f4ff6a5d4 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -58,10 +58,12 @@ let dependent_init =
   (* Goals are created with a store which marks them as unresolvable
      for type classes. *)
   let store = Typeclasses.set_resolvable Evd.Store.empty false in
+  (* Goals don't have a source location. *)
+  let src = (Loc.ghost,Evar_kinds.GoalEvar) in
+  (* Main routine *)
   let rec aux = function
   | TNil sigma -> [], { solution = sigma; comb = []; }
   | TCons (env, sigma, typ, t) ->
-    let src = (Loc.ghost,Evar_kinds.GoalEvar) in
     let (sigma, econstr ) = Evarutil.new_evar env sigma ~src ~store typ in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let (gl, _) = Term.destEvar econstr in
-- 
cgit v1.2.3