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.

1 files changed, 3 insertions, 1 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 827fe56a6..7f4ff6a5d 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