aboutsummaryrefslogtreecommitdiff
path: root/engine/proofview.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/proofview.ml')
-rw-r--r--engine/proofview.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 333ae78b3a..21227ed198 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -22,6 +22,8 @@ open Context.Named.Declaration
(** Main state of tactics *)
type proofview = Proofview_monad.proofview
+(* The first items in pairs below are proofs (under construction).
+ The second items in the pairs below are statements that are being proved. *)
type entry = (Term.constr * Term.types) list
(** Returns a stylised view of a proofview for use by, for instance,