aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/obligations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/obligations.ml')
-rw-r--r--vernac/obligations.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index fa6a9adf1..1f401b4e1 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -40,7 +40,7 @@ let check_evars env evm =
type oblinfo =
{ ev_name: int * Id.t;
- ev_hyps: Context.Named.t;
+ ev_hyps: Constr.named_context;
ev_status: bool * Evar_kinds.obligation_definition_status;
ev_chop: int option;
ev_src: Evar_kinds.t Loc.located;