aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/proofview_monad.ml4
-rw-r--r--engine/proofview_monad.mli4
2 files changed, 4 insertions, 4 deletions
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 2b9db60b4..6f52b3ee9 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 7a6ea10fe..0aff0a720 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} *)