aboutsummaryrefslogtreecommitdiff
path: root/checker/declarations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/declarations.ml')
-rw-r--r--checker/declarations.ml6
1 files changed, 2 insertions, 4 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 5034604220..69dd261308 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -139,10 +139,8 @@ let solve_delta_kn resolve kn =
make_kn new_mp dir l
let gen_of_delta resolve x kn fix_can =
- try
- let new_kn = solve_delta_kn resolve kn in
- if kn == new_kn then x else fix_can new_kn
- with _ -> x
+ let new_kn = solve_delta_kn resolve kn in
+ if kn == new_kn then x else fix_can new_kn
let constant_of_delta resolve con =
let kn = user_con con in