From 61ee00dc214599ab6b17fac0586c746563eb565d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 7 Apr 2014 12:08:15 +0200
Subject: Transfering the initial goals from the proofview to the proof object.
 They were just passed along in the tactics.

---
 bootstrap/Monads.v | 1 -
 1 file changed, 1 deletion(-)

(limited to 'bootstrap')

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index 10defd0f98..40e26e20a2 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -567,7 +567,6 @@ Extract Inlined Constant goal => "Goal.goal".
 Extract Inlined Constant env => "Environ.env".
 
 Record proofview := {
-  initial : list (constr*types);
   solution : evar_map;
   comb : list goal
 }.
-- 
cgit v1.2.3