From b2a2cb77f38549a25417d199e90d745715f3e465 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 18:08:42 +0100
Subject: Making Proofview independent of Logic.

---
 engine/proofview_monad.ml  | 4 ++--
 engine/proofview_monad.mli | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'engine')

diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 2b9db60b4f..6f52b3ee90 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -154,8 +154,8 @@ end
     focused goals. *)
 type proofview = {
   solution : Evd.evar_map;
-  comb : Goal.goal list;
-  shelf : Goal.goal list;
+  comb : Evar.t list;
+  shelf : Evar.t list;
 }
 
 (** {6 Instantiation of the logic monad} *)
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 7a6ea10fe3..0aff0a7207 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -70,8 +70,8 @@ end
     focused goals. *)
 type proofview = {
   solution : Evd.evar_map;
-  comb : Goal.goal list;
-  shelf : Goal.goal list;
+  comb : Evar.t list;
+  shelf : Evar.t list;
 }
 
 (** {6 Instantiation of the logic monad} *)
-- 
cgit v1.2.3