aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proofview.mli')
-rw-r--r--proofs/proofview.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index a92abcbbf..aac56e565 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -446,7 +446,7 @@ module Goal : sig
environment of [gl] (i.e. the global environment and the
hypotheses) and the current evar map. *)
val concl : ([ `NF ], 'r) t -> Term.constr
- val hyps : ([ `NF ], 'r) t -> Context.named_context
+ val hyps : ([ `NF ], 'r) t -> Context.Named.t
val env : ('a, 'r) t -> Environ.env
val sigma : ('a, 'r) t -> 'r Sigma.t
val extra : ('a, 'r) t -> Evd.Store.t