From 5474d83bc8845bd5aa3fb339057d6efa5feedd7a Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 25 Oct 2016 13:29:43 +0200 Subject: COMMENT: Proofview.entry --- engine/proofview.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index 333ae78b3..21227ed19 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, -- cgit v1.2.3