aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof.ml')
-rw-r--r--proofs/proof.ml12
1 files changed, 5 insertions, 7 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 9e6045661..aafacaeb3 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -326,11 +326,9 @@ module V82 = struct
{ p with proofview = Proofview.V82.grab p.proofview }
- let instantiate_evar n com pr =
- let sp = pr.proofview in
- try
- let new_proofview = Proofview.V82.instantiate_evar n com sp in
- { pr with proofview = new_proofview }
- with e ->
- raise e
+ let instantiate_evar n com pr =
+ let sp = pr.proofview in
+ let new_proofview = Proofview.V82.instantiate_evar n com sp in
+ { pr with proofview = new_proofview }
+
end