diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml index 44c155089644d820e7d7f2834f3e162e75ed7908..56025255e45d37c6806d620a53ba8efc4ce4fcad 100644 --- a/src/kernel_services/ast_queries/ast_diff.ml +++ b/src/kernel_services/ast_queries/ast_diff.ml @@ -1105,7 +1105,7 @@ and is_same_instr i i' env: body_correspondance*is_same_env = | Skip _, Skip _ -> `Same_body, env | Code_annot _, Code_annot _ -> (* should not be present in normalized AST *) - `Same_body, env + Kernel.fatal "Unexpected Code_annot instruction in normalized AST" | _ -> `Body_changed, env and is_same_instr_list l l' env =