aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_subst.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/mod_subst.ml')
-rw-r--r--kernel/mod_subst.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 8c768b3a5..8b11aa185 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -643,7 +643,7 @@ let update_delta_resolver resolver1 resolver2 =
Change_equiv_to_inline c ->
Deltamap.add key (Inline (Some c)) res)
| _ -> Deltamap.add key hint res
- with not_found ->
+ with Not_found ->
Deltamap.add key hint res
in
Deltamap.fold apply_res resolver1 empty_delta_resolver