aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proofview.ml')
-rw-r--r--proofs/proofview.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index bdddf310d..823082ace 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -686,7 +686,7 @@ module Goal = struct
let env { env=env } = env
let sigma { sigma=sigma } = sigma
- let hyps { hyps=hyps } = hyps
+ let hyps { hyps=hyps } = Environ.named_context_of_val hyps
let concl { concl=concl } = concl
let lift s =