aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--proofs/proofview.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 80569e2342..6d7dcb9257 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1061,7 +1061,6 @@ struct
let typecheck_proof c concl env sigma =
let evdref = ref sigma in
let () = Typing.check env evdref c concl in
- Evarconv.check_problems_are_solved env !evdref;
!evdref
let (pr_constrv,pr_constr) =