diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-20 22:16:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:34 +0100 |
| commit | e09f3b44bb381854b647a6d9debdeddbfc49177e (patch) | |
| tree | e7ba5807fa369b912cb36fe50bba97d33f7af5b5 /engine/proofview.mli | |
| parent | d4b344acb23f19b089098b7788f37ea22bc07b81 (diff) | |
Proofview.Goal primitive now return EConstrs.
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 4 |
1 files changed, 2 insertions, 2 deletions
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 } |