From e09f3b44bb381854b647a6d9debdeddbfc49177e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 22:16:08 +0100 Subject: Proofview.Goal primitive now return EConstrs. --- engine/proofview.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/proofview.mli') diff --git a/engine/proofview.mli b/engine/proofview.mli index 725445251..2350592a2 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -484,7 +484,7 @@ module Goal : sig respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the hypotheses) and the current evar map. *) - val concl : ([ `NF ], 'r) t -> Term.constr + val concl : ([ `NF ], 'r) t -> EConstr.constr val hyps : ([ `NF ], 'r) t -> Context.Named.t val env : ('a, 'r) t -> Environ.env val sigma : ('a, 'r) t -> 'r Sigma.t @@ -492,7 +492,7 @@ module Goal : sig (** Returns the goal's conclusion even if the goal is not normalised. *) - val raw_concl : ('a, 'r) t -> Term.constr + val raw_concl : ('a, 'r) t -> EConstr.constr type ('a, 'b) enter = { enter : 'r. ('a, 'r) t -> 'b } -- cgit v1.2.3